harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean
lemma cexp_neg_quadratic_isLittleO_abs_rpow_cocompact {a : ℂ} (ha : a.re < 0) (b : ℂ) (s : ℝ) :
    (fun x : ℝ ↦ cexp (a * x ^ 2 + b * x)) =o[cocompact ℝ] (|·| ^ s)

Proof state:
case left
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ (fun x => cexp (a * ↑x ^ 2 + b * ↑x)) =o[atBot] fun x => |x| ^ s

Tactic:
refine ((cexp_neg_quadratic_isLittleO_rpow_atTop ha (-b) s).comp_tendsto
  Filter.tendsto_neg_atBot_atTop).congr' (Eventually.of_forall fun x ↦ ?_) ?_

Result:
case left.refine_1
a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
⊢ ((fun x => cexp (a * ↑x ^ 2 + -b * ↑x)) ∘ Neg.neg) x = (fun x => cexp (a * ↑x ^ 2 + b * ↑x)) x

case left.refine_2
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ (fun x => x ^ s) ∘ Neg.neg =ᶠ[atBot] fun x => |x| ^ s

Proof state:
case right
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ (fun x => cexp (a * ↑x ^ 2 + b * ↑x)) =o[atTop] fun x => |x| ^ s

Tactic:
refine (cexp_neg_quadratic_isLittleO_rpow_atTop ha b s).congr' EventuallyEq.rfl ?_

Result:
case right
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ (fun x => x ^ s) =ᶠ[atTop] fun x => |x| ^ s

Proof state:
case left.refine_2
a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
hx : x < 0
⊢ ((fun x => x ^ s) ∘ Neg.neg) x = (fun x => |x| ^ s) x

Tactic:
simp only [Function.comp_apply, abs_of_neg hx]

Result:
no goals

Proof state:
case left.refine_2
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ (fun x => x ^ s) ∘ Neg.neg =ᶠ[atBot] fun x => |x| ^ s

Tactic:
refine (eventually_lt_atBot 0).mp (Eventually.of_forall fun x hx ↦ ?_)

Result:
case left.refine_2
a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
hx : x < 0
⊢ ((fun x => x ^ s) ∘ Neg.neg) x = (fun x => |x| ^ s) x

Proof state:
case left.refine_1
a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
⊢ ((fun x => cexp (a * ↑x ^ 2 + -b * ↑x)) ∘ Neg.neg) x = (fun x => cexp (a * ↑x ^ 2 + b * ↑x)) x

Tactic:
simp only [neg_mul, Function.comp_apply, ofReal_neg, neg_sq, mul_neg, neg_neg]

Result:
no goals

Proof state:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ ((fun x => cexp (a * ↑x ^ 2 + b * ↑x)) =o[atBot] fun x => |x| ^ s) ∧
    (fun x => cexp (a * ↑x ^ 2 + b * ↑x)) =o[atTop] fun x => |x| ^ s

Tactic:
constructor

Result:
case left
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ (fun x => cexp (a * ↑x ^ 2 + b * ↑x)) =o[atBot] fun x => |x| ^ s

case right
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ (fun x => cexp (a * ↑x ^ 2 + b * ↑x)) =o[atTop] fun x => |x| ^ s

Proof state:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ (fun x => cexp (a * ↑x ^ 2 + b * ↑x)) =o[cocompact ℝ] fun x => |x| ^ s

Tactic:
rw [cocompact_eq_atBot_atTop, isLittleO_sup]

Result:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ ((fun x => cexp (a * ↑x ^ 2 + b * ↑x)) =o[atBot] fun x => |x| ^ s) ∧
    (fun x => cexp (a * ↑x ^ 2 + b * ↑x)) =o[atTop] fun x => |x| ^ s

Proof state:
case right
a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
hx : 0 < x
⊢ (fun x => x ^ s) x = (fun x => |x| ^ s) x

Tactic:
simp_rw [abs_of_pos hx]

Result:
no goals

Proof state:
case right
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ (fun x => x ^ s) =ᶠ[atTop] fun x => |x| ^ s

Tactic:
refine (eventually_gt_atTop 0).mp (Eventually.of_forall fun x hx ↦ ?_)

Result:
case right
a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
hx : 0 < x
⊢ (fun x => x ^ s) x = (fun x => |x| ^ s) x
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem isLittleO_one_exp_comp {f : α → ℝ} :
    ((fun _ => 1 : α → ℝ) =o[l] fun x => exp (f x)) ↔ Tendsto f l atTop

Proof state:
α : Type u_1
l : Filter α
f : α → ℝ
⊢ ((fun x => 1) =o[l] fun x => rexp (f x)) ↔ Tendsto f l atTop

Tactic:
simp only [← exp_zero, isLittleO_exp_comp_exp_comp, sub_zero]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Tendsto.lean
theorem OrderTop.atTop_eq (α) [PartialOrder α] [OrderTop α] : (atTop : Filter α) = pure ⊤

Proof state:
α : Type u_6
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
⊢ atTop = pure ⊤

Tactic:
rw [isTop_top.atTop_eq, Ici_top, principal_singleton]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/OfAddContent.lean
theorem isCaratheodory_inducedOuterMeasure (hC : IsSetSemiring C) (m : AddContent C)
    (s : Set α) (hs : MeasurableSet[MeasurableSpace.generateFrom C] s) :
    (inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty).IsCaratheodory s

Proof state:
case basic
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
m : AddContent C
s u : Set α
hu : u ∈ C
⊢ (inducedOuterMeasure (fun x x_1 => m x) ⋯ ⋯).IsCaratheodory u

Tactic:
exact isCaratheodory_inducedOuterMeasure_of_mem hC m hu

Result:
no goals

Proof state:
case empty
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
m : AddContent C
s : Set α
⊢ (inducedOuterMeasure (fun x x_1 => m x) ⋯ ⋯).IsCaratheodory ∅

Tactic:
exact OuterMeasure.isCaratheodory_empty _

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
m : AddContent C
s : Set α
hs : MeasurableSet s
⊢ (inducedOuterMeasure (fun x x_1 => m x) ⋯ ⋯).IsCaratheodory s

Tactic:
induction hs with
| basic u hu => exact isCaratheodory_inducedOuterMeasure_of_mem hC m hu
| empty => exact OuterMeasure.isCaratheodory_empty _
| compl t _ h => exact OuterMeasure.isCaratheodory_compl _ h
| iUnion f _ h => exact OuterMeasure.isCaratheodory_iUnion _ h

Result:
no goals

Proof state:
case compl
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
m : AddContent C
s t : Set α
a✝ : MeasurableSpace.GenerateMeasurable C t
h : (inducedOuterMeasure (fun x x_1 => m x) ⋯ ⋯).IsCaratheodory t
⊢ (inducedOuterMeasure (fun x x_1 => m x) ⋯ ⋯).IsCaratheodory tᶜ

Tactic:
exact OuterMeasure.isCaratheodory_compl _ h

Result:
no goals

Proof state:
case iUnion
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
m : AddContent C
s : Set α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), MeasurableSpace.GenerateMeasurable C (f n)
h : ∀ (n : ℕ), (inducedOuterMeasure (fun x x_1 => m x) ⋯ ⋯).IsCaratheodory (f n)
⊢ (inducedOuterMeasure (fun x x_1 => m x) ⋯ ⋯).IsCaratheodory (⋃ i, f i)

Tactic:
exact OuterMeasure.isCaratheodory_iUnion _ h

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
theorem maxGenEigenspace_eq_genEigenspace_finrank
    [FiniteDimensional K V] (f : End K V) (μ : K) :
    f.maxGenEigenspace μ = f.genEigenspace μ (finrank K V)

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ (f.genEigenspace μ) ⊤ ≤ (f.genEigenspace μ) ↑(finrank K V)

Tactic:
rw [genEigenspace_top_eq_maxUnifEigenspaceIndex]

Result:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ) ≤ (f.genEigenspace μ) ↑(finrank K V)

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ) ≤ (f.genEigenspace μ) ↑(finrank K V)

Tactic:
apply genEigenspace_le_genEigenspace_finrank f μ

Result:
no goals

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ f.maxGenEigenspace μ = (f.genEigenspace μ) ↑(finrank K V)

Tactic:
apply le_antisymm _ <| (f.genEigenspace μ).monotone le_top

Result:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ (f.genEigenspace μ) ⊤ ≤ (f.genEigenspace μ) ↑(finrank K V)
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
@[simp] lemma deleteEdges_eq_self : G.deleteEdges s = G ↔ Disjoint G.edgeSet s

Proof state:
V : Type u
G : SimpleGraph V
s : Set (Sym2 V)
⊢ G.deleteEdges s = G ↔ Disjoint G.edgeSet s

Tactic:
rw [deleteEdges, sdiff_eq_left, disjoint_fromEdgeSet]

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/Isometry.lean
theorem linear_eq_linear_isometry : e.linear = e.linearIsometryEquiv.toLinearEquiv

Proof state:
case h
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
e : P ≃ᵃⁱ[𝕜] P₂
x✝ : V
⊢ e.linear x✝ = e.linearIsometryEquiv.toLinearEquiv x✝

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
e : P ≃ᵃⁱ[𝕜] P₂
⊢ e.linear = e.linearIsometryEquiv.toLinearEquiv

Tactic:
ext

Result:
case h
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
e : P ≃ᵃⁱ[𝕜] P₂
x✝ : V
⊢ e.linear x✝ = e.linearIsometryEquiv.toLinearEquiv x✝
-- Mathlib/Geometry/RingedSpace/PresheafedSpace.lean
theorem congr_app {X Y : PresheafedSpace C} {α β : X ⟶ Y} (h : α = β) (U) :
    α.c.app U = β.c.app U ≫ X.presheaf.map (eqToHom (by subst h; rfl))

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
α β : X ⟶ Y
h : α = β
U : (Opens ↑↑Y)ᵒᵖ
⊢ α.c.app U = β.c.app U ≫ X.presheaf.map (eqToHom ⋯)

Tactic:
subst h

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
α : X ⟶ Y
U : (Opens ↑↑Y)ᵒᵖ
⊢ α.c.app U = α.c.app U ≫ X.presheaf.map (eqToHom ⋯)

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
α : X ⟶ Y
U : (Opens ↑↑Y)ᵒᵖ
⊢ α.c.app U = α.c.app U ≫ X.presheaf.map (eqToHom ⋯)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{?u.23625, u_1} C
X Y : PresheafedSpace C
α : X ⟶ Y
U : (Opens ↑↑Y)ᵒᵖ
⊢ (Opens.map α.base).op.obj U = (Opens.map α.base).op.obj U

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{?u.23625, u_1} C
X Y : PresheafedSpace C
α β : X ⟶ Y
h : α = β
U : (Opens ↑↑Y)ᵒᵖ
⊢ (Opens.map β.base).op.obj U = (Opens.map α.base).op.obj U

Tactic:
subst h

Result:
C : Type u_1
inst✝ : Category.{?u.23625, u_1} C
X Y : PresheafedSpace C
α : X ⟶ Y
U : (Opens ↑↑Y)ᵒᵖ
⊢ (Opens.map α.base).op.obj U = (Opens.map α.base).op.obj U
-- Mathlib/CategoryTheory/Localization/Triangulated.lean
lemma distTriang_iff (T : Triangle D) :
    (T ∈ distTriang D) ↔ T ∈ L.essImageDistTriang

Proof state:
case mp
C : Type u_1
D : Type u_2
inst✝¹⁴ : Category.{u_4, u_1} C
inst✝¹³ : Category.{u_3, u_2} D
L : C ⥤ D
inst✝¹² : HasShift C ℤ
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁸ : Pretriangulated C
inst✝⁷ : HasShift D ℤ
inst✝⁶ : L.CommShift ℤ
inst✝⁵ : HasZeroObject D
inst✝⁴ : Preadditive D
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
inst✝¹ : L.mapArrow.EssSurj
inst✝ : L.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
⊢ T ∈ L.essImageDistTriang

Tactic:
let f := L.mapArrow.objPreimage T.mor₁

Result:
case mp
C : Type u_1
D : Type u_2
inst✝¹⁴ : Category.{u_4, u_1} C
inst✝¹³ : Category.{u_3, u_2} D
L : C ⥤ D
inst✝¹² : HasShift C ℤ
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁸ : Pretriangulated C
inst✝⁷ : HasShift D ℤ
inst✝⁶ : L.CommShift ℤ
inst✝⁵ : HasZeroObject D
inst✝⁴ : Preadditive D
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
inst✝¹ : L.mapArrow.EssSurj
inst✝ : L.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
f : Arrow C := L.mapArrow.objPreimage (Arrow.mk T.mor₁)
⊢ T ∈ L.essImageDistTriang
-- Mathlib/Order/Filter/Basic.lean
theorem principal_eq_iff_eq {s t : Set α} : 𝓟 s = 𝓟 t ↔ s = t

Proof state:
α : Type u
s t : Set α
⊢ 𝓟 s = 𝓟 t ↔ s = t

Tactic:
simp only [le_antisymm_iff, le_principal_iff, mem_principal]

Result:
α : Type u
s t : Set α
⊢ s ⊆ t ∧ t ⊆ s ↔ s ≤ t ∧ t ≤ s

Proof state:
α : Type u
s t : Set α
⊢ s ⊆ t ∧ t ⊆ s ↔ s ≤ t ∧ t ≤ s

Tactic:
rfl

Result:
no goals
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma isTheta_deriv_rpow_p_mul_one_add_smoothingFn {p : ℝ} (hp : p ≠ 0) :
    (fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖) =Θ[atTop] fun z => z ^ (p-1)

Proof state:
p : ℝ
hp : p ≠ 0
⊢ (deriv fun z => z ^ p * (1 + ε z)) =Θ[atTop] fun z => z ^ (p - 1)

Tactic:
calc (fun x => deriv (fun z => z ^ p * (1 + ε z)) x) =Θ[atTop] fun z => p * z ^ (p-1) :=
          (isEquivalent_deriv_rpow_p_mul_one_add_smoothingFn hp).isTheta
  _ =Θ[atTop] fun z => z ^ (p-1) :=
          IsTheta.const_mul_left hp <| isTheta_refl _ _

Result:
no goals

Proof state:
p : ℝ
hp : p ≠ 0
⊢ (fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖) =Θ[atTop] fun z => z ^ (p - 1)

Tactic:
refine IsTheta.norm_left ?_

Result:
p : ℝ
hp : p ≠ 0
⊢ (deriv fun z => z ^ p * (1 + ε z)) =Θ[atTop] fun z => z ^ (p - 1)
-- Mathlib/NumberTheory/Modular.lean
theorem three_le_four_mul_im_sq_of_mem_fd {τ : ℍ} (h : τ ∈ 𝒟) : 3 ≤ 4 * τ.im ^ 2

Proof state:
τ : ℍ
h : τ ∈ 𝒟
this : 1 ≤ τ.re * τ.re + τ.im * τ.im
⊢ 3 ≤ 4 * τ.im ^ 2

Tactic:
cases abs_cases τ.re <;> nlinarith [h.2]

Result:
no goals

Proof state:
τ : ℍ
h : τ ∈ 𝒟
⊢ 1 ≤ τ.re * τ.re + τ.im * τ.im

Tactic:
simpa [Complex.normSq_apply] using h.1

Result:
no goals

Proof state:
τ : ℍ
h : τ ∈ 𝒟
⊢ 3 ≤ 4 * τ.im ^ 2

Tactic:
have : 1 ≤ τ.re * τ.re + τ.im * τ.im := by simpa [Complex.normSq_apply] using h.1

Result:
τ : ℍ
h : τ ∈ 𝒟
this : 1 ≤ τ.re * τ.re + τ.im * τ.im
⊢ 3 ≤ 4 * τ.im ^ 2
-- Mathlib/CategoryTheory/Monoidal/End.lean
theorem obj_μ_app (m₁ m₂ m₃ : M) (X : C) [F.Monoidal] :
    (F.obj m₃).map ((μ F m₁ m₂).app X) =
      (μ F m₂ m₃).app ((F.obj m₁).obj X) ≫
        (μ F m₁ (m₂ ⊗ m₃)).app X ≫
          (F.map (α_ m₁ m₂ m₃).inv).app X ≫ (δ F (m₁ ⊗ m₂) m₃).app X

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ m₃ : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj m₃).map ((μ F m₁ m₂).app X) =
    (F.obj m₃).map ((μ F m₁ m₂).app X) ≫
      (μ F (m₁ ⊗ m₂) m₃).app X ≫
        (F.map (α_ m₁ m₂ m₃).hom).app X ≫ (F.map (α_ m₁ m₂ m₃).inv).app X ≫ (δ F (m₁ ⊗ m₂) m₃).app X

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ m₃ : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj m₃).map ((μ F m₁ m₂).app X) =
    (μ F m₂ m₃).app ((F.obj m₁).obj X) ≫
      (μ F m₁ (m₂ ⊗ m₃)).app X ≫ (F.map (α_ m₁ m₂ m₃).inv).app X ≫ (δ F (m₁ ⊗ m₂) m₃).app X

Tactic:
rw [← associativity_app_assoc]

Result:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ m₃ : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj m₃).map ((μ F m₁ m₂).app X) =
    (F.obj m₃).map ((μ F m₁ m₂).app X) ≫
      (μ F (m₁ ⊗ m₂) m₃).app X ≫
        (F.map (α_ m₁ m₂ m₃).hom).app X ≫ (F.map (α_ m₁ m₂ m₃).inv).app X ≫ (δ F (m₁ ⊗ m₂) m₃).app X
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
theorem iSupLift_of_mem {i : ι} (x : T) (hx : (x : A) ∈ K i) :
    iSupLift K dir f hf T hT x = f i ⟨x, hx⟩

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i : ι
x : ↥(iSup K)
hx : ↑x ∈ K i
⊢ (iSupLift K dir f hf (iSup K) ⋯) x = (f i) ⟨↑x, hx⟩

Tactic:
dsimp [iSupLift]

Result:
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i : ι
x : ↥(iSup K)
hx : ↑x ∈ K i
⊢ Set.iUnionLift (fun i => ↑(K i)) (fun i x => (f i) x) ⋯ ↑(iSup K) ⋯ x = (f i) ⟨↑x, hx⟩

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalSubalgebra R A
hT : T = iSup K
i : ι
x : ↥T
hx : ↑x ∈ K i
⊢ (iSupLift K dir f hf T hT) x = (f i) ⟨↑x, hx⟩

Tactic:
subst hT

Result:
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i : ι
x : ↥(iSup K)
hx : ↑x ∈ K i
⊢ (iSupLift K dir f hf (iSup K) ⋯) x = (f i) ⟨↑x, hx⟩

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i : ι
x : ↥(iSup K)
hx : ↑x ∈ K i
⊢ Set.iUnionLift (fun i => ↑(K i)) (fun i x => (f i) x) ⋯ ↑(iSup K) ⋯ x = (f i) ⟨↑x, hx⟩

Tactic:
apply Set.iUnionLift_of_mem

Result:
no goals
-- Mathlib/Analysis/VonNeumannAlgebra/Basic.lean
theorem commutant_commutant (S : VonNeumannAlgebra H) : S.commutant.commutant = S :=
  SetLike.coe_injective <| by simp

Proof state:
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
⊢ ↑S.commutant.commutant = ↑S

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem length_mapIdx_go : ∀ {l : List α} {arr : Array β},
    (mapIdx.go f l arr).length = l.length + arr.size
  | [], _ => by simp [mapIdx.go]
  | a :: l, _ => by
    simp only [mapIdx.go, length_cons]
    rw [length_mapIdx_go]
    simp
    omega

Proof state:
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
x✝ : Array β
⊢ (mapIdx.go f (a :: l) x✝).length = (a :: l).length + x✝.size

Tactic:
simp only [mapIdx.go, length_cons]

Result:
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
x✝ : Array β
⊢ (mapIdx.go f l (x✝.push (f x✝.size a))).length = l.length + 1 + x✝.size

Proof state:
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
x✝ : Array β
⊢ l.length + (x✝.push (f x✝.size a)).size = l.length + 1 + x✝.size

Tactic:
simp

Result:
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
x✝ : Array β
⊢ l.length + (x✝.size + 1) = l.length + 1 + x✝.size

Proof state:
α : Type u_1
β : Type u_2
f : Nat → α → β
x✝ : Array β
⊢ (mapIdx.go f [] x✝).length = [].length + x✝.size

Tactic:
simp [mapIdx.go]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
x✝ : Array β
⊢ (mapIdx.go f l (x✝.push (f x✝.size a))).length = l.length + 1 + x✝.size

Tactic:
rw [length_mapIdx_go]

Result:
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
x✝ : Array β
⊢ l.length + (x✝.push (f x✝.size a)).size = l.length + 1 + x✝.size

Proof state:
α : Type u_1
β : Type u_2
f : Nat → α → β
a : α
l : List α
x✝ : Array β
⊢ l.length + (x✝.size + 1) = l.length + 1 + x✝.size

Tactic:
omega

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
theorem Multipliable.tendsto_atTop_one {f : ℕ → G} (hf : Multipliable f) :
    Tendsto f atTop (𝓝 1)

Proof state:
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℕ → G
hf : Multipliable f
⊢ Tendsto f atTop (𝓝 1)

Tactic:
rw [← Nat.cofinite_eq_atTop]

Result:
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℕ → G
hf : Multipliable f
⊢ Tendsto f cofinite (𝓝 1)

Proof state:
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℕ → G
hf : Multipliable f
⊢ Tendsto f cofinite (𝓝 1)

Tactic:
exact hf.tendsto_cofinite_one

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem Topology.IsInducing.isCompact_iff {f : X → Y} (hf : IsInducing f) :
    IsCompact s ↔ IsCompact (f '' s)

Proof state:
case intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
hs : IsCompact (f '' s)
F : Filter X
F_ne_bot : F.NeBot
F_le : F ≤ 𝓟 s
x : X
x_in : x ∈ s
hx : ClusterPt (f x) (map f F)
⊢ ∃ x ∈ s, ClusterPt x F

Tactic:
exact ⟨x, x_in, hf.mapClusterPt_iff.1 hx⟩

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
hs : IsCompact (f '' s)
F : Filter X
F_ne_bot : F.NeBot
F_le : F ≤ 𝓟 s
⊢ ∃ x ∈ s, ClusterPt x F

Tactic:
obtain ⟨_, ⟨x, x_in : x ∈ s, rfl⟩, hx : ClusterPt (f x) (map f F)⟩ :=
  hs ((map_mono F_le).trans_eq map_principal)

Result:
case intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
hs : IsCompact (f '' s)
F : Filter X
F_ne_bot : F.NeBot
F_le : F ≤ 𝓟 s
x : X
x_in : x ∈ s
hx : ClusterPt (f x) (map f F)
⊢ ∃ x ∈ s, ClusterPt x F

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ IsCompact s ↔ IsCompact (f '' s)

Tactic:
refine ⟨fun hs => hs.image hf.continuous, fun hs F F_ne_bot F_le => ?_⟩

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
hs : IsCompact (f '' s)
F : Filter X
F_ne_bot : F.NeBot
F_le : F ≤ 𝓟 s
⊢ ∃ x ∈ s, ClusterPt x F
-- Mathlib/Probability/Kernel/Condexp.lean
theorem _root_.MeasureTheory.Integrable.comp_snd_map_prod_id [NormedAddCommGroup F] (hm : m ≤ mΩ)
    (hf : Integrable f μ) : Integrable (fun x : Ω × Ω => f x.2)
      (@Measure.map Ω (Ω × Ω) mΩ (m.prod mΩ) (fun ω => (id ω, id ω)) μ)

Proof state:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → F
inst✝ : NormedAddCommGroup F
hm : m ≤ mΩ
hf : Integrable (fun x => f x.2) (Measure.map (fun ω => (id ω, ω)) μ)
⊢ Integrable (fun x => f x.2) (Measure.map (fun ω => (id ω, id ω)) μ)

Tactic:
simp_rw [id] at hf ⊢

Result:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → F
inst✝ : NormedAddCommGroup F
hm : m ≤ mΩ
hf : Integrable (fun x => f x.2) (Measure.map (fun ω => (ω, ω)) μ)
⊢ Integrable (fun x => f x.2) (Measure.map (fun ω => (ω, ω)) μ)

Proof state:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → F
inst✝ : NormedAddCommGroup F
hm : m ≤ mΩ
hf : Integrable (fun x => f x.2) (Measure.map (fun ω => (ω, ω)) μ)
⊢ Integrable (fun x => f x.2) (Measure.map (fun ω => (ω, ω)) μ)

Tactic:
exact hf

Result:
no goals

Proof state:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → F
inst✝ : NormedAddCommGroup F
hm : m ≤ mΩ
hf : Integrable f μ
⊢ Integrable (fun x => f x.2) (Measure.map (fun ω => (id ω, id ω)) μ)

Tactic:
rw [← integrable_comp_snd_map_prod_mk_iff (measurable_id'' hm)] at hf

Result:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → F
inst✝ : NormedAddCommGroup F
hm : m ≤ mΩ
hf : Integrable (fun x => f x.2) (Measure.map (fun ω => (id ω, ω)) μ)
⊢ Integrable (fun x => f x.2) (Measure.map (fun ω => (id ω, id ω)) μ)