harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma eventually_deriv_rpow_p_mul_one_sub_smoothingFn (p : ℝ) :
    deriv (fun z => z ^ p * (1 - ε z))
      =ᶠ[atTop] fun z => p * z ^ (p-1) * (1 - ε z) + z ^ (p-1) / (log z ^ 2) := calc
  deriv (fun x => x ^ p * (1 - ε x))
    =ᶠ[atTop] fun x => deriv (· ^ p) x * (1 - ε x) + x ^ p * deriv (1 - ε ·) x

Proof state:
case h
p x : ℝ
hx : 0 < x
⊢ p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / log x ^ 2) = p * x ^ (p - 1) * (1 - ε x) + x ^ (p - 1) / log x ^ 2

Tactic:
rw [mul_div, ← Real.rpow_neg_one, ← Real.rpow_add (by positivity), sub_eq_add_neg]

Result:
no goals

Proof state:
case h.hc
p x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x ^ p) x

Tactic:
exact differentiableAt_rpow_const_of_ne _ (by positivity)

Result:
no goals

Proof state:
p : ℝ
⊢ (fun x => deriv (fun x => x ^ p) x * (1 - ε x) + x ^ p * deriv (fun x => 1 - ε x) x) =ᶠ[atTop] fun x =>
    p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / log x ^ 2)

Tactic:
filter_upwards [eventually_gt_atTop 1, eventually_deriv_one_sub_smoothingFn]
  with x hx hderiv

Result:
case h
p x : ℝ
hx : 1 < x
hderiv : deriv (fun x => 1 - ε x) x = x⁻¹ / log x ^ 2
⊢ deriv (fun x => x ^ p) x * (1 - ε x) + x ^ p * deriv (fun x => 1 - ε x) x =
    p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / log x ^ 2)

Proof state:
p : ℝ
⊢ (fun x => p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / log x ^ 2)) =ᶠ[atTop] fun x =>
    p * x ^ (p - 1) * (1 - ε x) + x ^ (p - 1) / log x ^ 2

Tactic:
filter_upwards [eventually_gt_atTop 0] with x hx

Result:
case h
p x : ℝ
hx : 0 < x
⊢ p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / log x ^ 2) = p * x ^ (p - 1) * (1 - ε x) + x ^ (p - 1) / log x ^ 2

Proof state:
case h.hd
p x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => 1 - ε x) x

Tactic:
exact differentiableAt_one_sub_smoothingFn hx

Result:
no goals

Proof state:
p x : ℝ
hx : 1 < x
hderiv : deriv (fun x => 1 - ε x) x = x⁻¹ / log x ^ 2
⊢ x ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
p x : ℝ
hx : 0 < x
⊢ 0 < x

Tactic:
positivity

Result:
no goals

Proof state:
p x : ℝ
hx : 1 < x
⊢ x ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case h
p x : ℝ
hx : 1 < x
⊢ deriv (fun x => x ^ p * (1 - ε x)) x = deriv (fun x => x ^ p) x * (1 - ε x) + x ^ p * deriv (fun x => 1 - ε x) x

Tactic:
rw [deriv_mul]

Result:
case h.hc
p x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => x ^ p) x

case h.hd
p x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (fun x => 1 - ε x) x

Proof state:
case h
p x : ℝ
hx : 1 < x
hderiv : deriv (fun x => 1 - ε x) x = x⁻¹ / log x ^ 2
⊢ deriv (fun x => x ^ p) x * (1 - ε x) + x ^ p * deriv (fun x => 1 - ε x) x =
    p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / log x ^ 2)

Tactic:
rw [hderiv, Real.deriv_rpow_const (Or.inl <| by positivity)]

Result:
no goals

Proof state:
p : ℝ
⊢ (deriv fun x => x ^ p * (1 - ε x)) =ᶠ[atTop] fun x =>
    deriv (fun x => x ^ p) x * (1 - ε x) + x ^ p * deriv (fun x => 1 - ε x) x

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx

Result:
case h
p x : ℝ
hx : 1 < x
⊢ deriv (fun x => x ^ p * (1 - ε x)) x = deriv (fun x => x ^ p) x * (1 - ε x) + x ^ p * deriv (fun x => 1 - ε x) x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mkArray_eq_append_iff {l₁ l₂ : Array α} {a : α} :
    mkArray n a = l₁ ++ l₂ ↔
      l₁.size + l₂.size = n ∧ l₁ = mkArray l₁.size a ∧ l₂ = mkArray l₂.size a

Proof state:
α : Type u_1
n : Nat
l₁ l₂ : Array α
a : α
⊢ mkArray n a = l₁ ++ l₂ ↔ l₁.size + l₂.size = n ∧ l₁ = mkArray l₁.size a ∧ l₂ = mkArray l₂.size a

Tactic:
rw [eq_comm, append_eq_mkArray_iff]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_cond_eq_right : (∏ᶠ (i) (_ : a = i), f i) = f a

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
⊢ ∏ᶠ (i : α) (_ : a = i), f i = f a

Tactic:
simp [@eq_comm _ a]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem q {hs : MeasurableSet s} {hμs : μ s ≠ ∞} {x : G} :
    MemLp (condExpIndSMul hm hs hμs x) 1 μ

Proof state:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : G
⊢ MemLp (↑↑(condExpIndSMul hm hs hμs x)) 1 μ

Tactic:
rw [memLp_one_iff_integrable]

Result:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : G
⊢ Integrable (↑↑(condExpIndSMul hm hs hμs x)) μ

Proof state:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : G
⊢ Integrable (↑↑(condExpIndSMul hm hs hμs x)) μ

Tactic:
apply integrable_condExpIndSMul

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tsum_coe_ne_top_iff_summable {f : β → ℝ≥0} : (∑' b, (f b : ℝ≥0∞)) ≠ ∞ ↔ Summable f

Proof state:
case intro
β : Type u_2
f : β → ℝ≥0
a : ℝ≥0
ha : ↑a = ∑' (b : β), ↑(f b)
⊢ Summable f

Tactic:
refine ⟨a, ENNReal.hasSum_coe.1 ?_⟩

Result:
case intro
β : Type u_2
f : β → ℝ≥0
a : ℝ≥0
ha : ↑a = ∑' (b : β), ↑(f b)
⊢ HasSum (fun a => ↑(f a)) ↑a

Proof state:
case intro
β : Type u_2
f : β → ℝ≥0
a : ℝ≥0
ha : ↑a = ∑' (b : β), ↑(f b)
⊢ HasSum (fun a => ↑(f a)) (∑' (b : β), ↑(f b))

Tactic:
exact ENNReal.summable.hasSum

Result:
no goals

Proof state:
β : Type u_2
f : β → ℝ≥0
⊢ ∑' (b : β), ↑(f b) ≠ ⊤ ↔ Summable f

Tactic:
refine ⟨fun h => ?_, fun h => ENNReal.coe_tsum h ▸ ENNReal.coe_ne_top⟩

Result:
β : Type u_2
f : β → ℝ≥0
h : ∑' (b : β), ↑(f b) ≠ ⊤
⊢ Summable f

Proof state:
β : Type u_2
f : β → ℝ≥0
h : ∑' (b : β), ↑(f b) ≠ ⊤
⊢ Summable f

Tactic:
lift ∑' b, (f b : ℝ≥0∞) to ℝ≥0 using h with a ha

Result:
case intro
β : Type u_2
f : β → ℝ≥0
a : ℝ≥0
ha : ↑a = ∑' (b : β), ↑(f b)
⊢ Summable f

Proof state:
case intro
β : Type u_2
f : β → ℝ≥0
a : ℝ≥0
ha : ↑a = ∑' (b : β), ↑(f b)
⊢ HasSum (fun a => ↑(f a)) ↑a

Tactic:
rw [ha]

Result:
case intro
β : Type u_2
f : β → ℝ≥0
a : ℝ≥0
ha : ↑a = ∑' (b : β), ↑(f b)
⊢ HasSum (fun a => ↑(f a)) (∑' (b : β), ↑(f b))
-- Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean
theorem one_add_norm_le_sqrt_two_mul_sqrt (x : E) :
    (1 : ℝ) + ‖x‖ ≤ √2 * √(1 + ‖x‖ ^ 2)

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
this : 0 ≤ (‖x‖ - 1) ^ 2
⊢ 1 + ‖x‖ ≤ √(2 * (1 + ‖x‖ ^ 2))

Tactic:
apply le_sqrt_of_sq_le

Result:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
this : 0 ≤ (‖x‖ - 1) ^ 2
⊢ (1 + ‖x‖) ^ 2 ≤ 2 * (1 + ‖x‖ ^ 2)

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
⊢ 1 + ‖x‖ ≤ √(2 * (1 + ‖x‖ ^ 2))

Tactic:
have := sq_nonneg (‖x‖ - 1)

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
this : 0 ≤ (‖x‖ - 1) ^ 2
⊢ 1 + ‖x‖ ≤ √(2 * (1 + ‖x‖ ^ 2))

Proof state:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
this : 0 ≤ (‖x‖ - 1) ^ 2
⊢ (1 + ‖x‖) ^ 2 ≤ 2 * (1 + ‖x‖ ^ 2)

Tactic:
linarith

Result:
no goals

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
⊢ 1 + ‖x‖ ≤ √2 * √(1 + ‖x‖ ^ 2)

Tactic:
rw [← sqrt_mul zero_le_two]

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
⊢ 1 + ‖x‖ ≤ √(2 * (1 + ‖x‖ ^ 2))
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem derivWithin_mul_const (hc : DifferentiableWithinAt 𝕜 c s x) (d : 𝔸) :
    derivWithin (fun y => c y * d) s x = derivWithin c s x * d

Proof state:
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
d : 𝔸
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => c y * d) s x = derivWithin c s x * d

Tactic:
exact (hc.hasDerivWithinAt.mul_const d).derivWithin hxs

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
d : 𝔸
⊢ derivWithin (fun y => c y * d) s x = derivWithin c s x * d

Tactic:
rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs

Result:
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
d : 𝔸
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => c y * d) s x = derivWithin c s x * d

case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
d : 𝔸
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => c y * d) s x = derivWithin c s x * d

Proof state:
case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
d : 𝔸
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => c y * d) s x = derivWithin c s x * d

Tactic:
simp [derivWithin_zero_of_isolated hxs]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem centroid_pair_fin [Invertible (2 : k)] (p : Fin 2 → P) :
    univ.centroid k p = (2⁻¹ : k) • (p 1 -ᵥ p 0) +ᵥ p 0

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Invertible 2
p : Fin 2 → P
⊢ centroid k {0, 1} p = 2⁻¹ • (p 1 -ᵥ p 0) +ᵥ p 0

Tactic:
convert centroid_pair k p 0 1

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Invertible 2
p : Fin 2 → P
⊢ centroid k univ p = 2⁻¹ • (p 1 -ᵥ p 0) +ᵥ p 0

Tactic:
rw [univ_fin2]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Invertible 2
p : Fin 2 → P
⊢ centroid k {0, 1} p = 2⁻¹ • (p 1 -ᵥ p 0) +ᵥ p 0
-- Mathlib/Data/PNat/Prime.lean
theorem coprime_coe {m n : ℕ+} : Nat.Coprime ↑m ↑n ↔ m.Coprime n

Proof state:
m n : ℕ+
⊢ (↑m).Coprime ↑n ↔ m.Coprime n

Tactic:
unfold Nat.Coprime Coprime

Result:
m n : ℕ+
⊢ (↑m).gcd ↑n = 1 ↔ m.gcd n = 1

Proof state:
m n : ℕ+
⊢ (↑m).gcd ↑n = 1 ↔ ↑(m.gcd n) = ↑1

Tactic:
simp

Result:
no goals

Proof state:
m n : ℕ+
⊢ (↑m).gcd ↑n = 1 ↔ m.gcd n = 1

Tactic:
rw [← coe_inj]

Result:
m n : ℕ+
⊢ (↑m).gcd ↑n = 1 ↔ ↑(m.gcd n) = ↑1
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma reflection_perm_involutive : Involutive (P.reflection_perm i) :=
  involutive_iff_iter_2_eq_id.mpr (by ext; simp)

Proof state:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i x✝ : ι
⊢ (⇑(P.reflection_perm i))^[2] x✝ = id x✝

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
⊢ (⇑(P.reflection_perm i))^[2] = id

Tactic:
ext

Result:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i x✝ : ι
⊢ (⇑(P.reflection_perm i))^[2] x✝ = id x✝
-- Mathlib/Algebra/Ring/Subring/MulOpposite.lean
theorem op_closure (s : Set R) : (closure s).op = closure (MulOpposite.unop ⁻¹' s)

Proof state:
case e_a.h
R : Type u_2
inst✝ : Ring R
s : Set R
a : Subring Rᵐᵒᵖ
⊢ a ∈ {a | s ⊆ MulOpposite.op ⁻¹' ↑a} ↔ a ∈ {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}

Tactic:
exact MulOpposite.unop_surjective.forall

Result:
no goals

Proof state:
R : Type u_2
inst✝ : Ring R
s : Set R
⊢ sInf {a | s ⊆ MulOpposite.op ⁻¹' ↑a} = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}

Tactic:
congr with a

Result:
case e_a.h
R : Type u_2
inst✝ : Ring R
s : Set R
a : Subring Rᵐᵒᵖ
⊢ a ∈ {a | s ⊆ MulOpposite.op ⁻¹' ↑a} ↔ a ∈ {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}

Proof state:
R : Type u_2
inst✝ : Ring R
s : Set R
⊢ (closure s).op = closure (MulOpposite.unop ⁻¹' s)

Tactic:
simp_rw [closure, op_sInf, Set.preimage_setOf_eq, coe_unop]

Result:
R : Type u_2
inst✝ : Ring R
s : Set R
⊢ sInf {a | s ⊆ MulOpposite.op ⁻¹' ↑a} = sInf {S | MulOpposite.unop ⁻¹' s ⊆ ↑S}
-- Mathlib/Analysis/Calculus/FDeriv/Comp.lean
theorem HasFDerivWithinAt.iterate {f : E → E} {f' : E →L[𝕜] E}
    (hf : HasFDerivWithinAt f f' s x) (hx : f x = x) (hs : MapsTo f s s) (n : ℕ) :
    HasFDerivWithinAt f^[n] (f' ^ n) s x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivWithinAt f f' s x
hx : f x = x
hs : MapsTo f s s
n : ℕ
⊢ HasFDerivWithinAt f^[n] (f' ^ n) s x

Tactic:
refine HasFDerivAtFilter.iterate hf ?_ hx n

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivWithinAt f f' s x
hx : f x = x
hs : MapsTo f s s
n : ℕ
⊢ Tendsto f (𝓝[s] x) (𝓝[s] x)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivWithinAt f f' s x
hx : f x = x
hs : MapsTo f s s
n : ℕ
⊢ Tendsto f (𝓝[s] x) (𝓝[s] x)

Tactic:
rw [_root_.nhdsWithin]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivWithinAt f f' s x
hx : f x = x
hs : MapsTo f s s
n : ℕ
⊢ Tendsto f (𝓝 x ⊓ 𝓟 s) (𝓝 x ⊓ 𝓟 s)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivWithinAt f f' s x
hx : f x = x
hs : MapsTo f s s
n : ℕ
⊢ Tendsto f (𝓝 x ⊓ 𝓟 s) (𝓝 x ⊓ 𝓟 s)

Tactic:
convert tendsto_inf.2 ⟨hf.continuousWithinAt, _⟩

Result:
case h.e'_5.h.e'_3.h.e'_3
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivWithinAt f f' s x
hx : f x = x
hs : MapsTo f s s
n : ℕ
⊢ x = f x

case convert_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivWithinAt f f' s x
hx : f x = x
hs : MapsTo f s s
n : ℕ
⊢ Tendsto f (𝓝[s] x) (𝓟 s)

Proof state:
case h.e'_5.h.e'_3.h.e'_3
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivWithinAt f f' s x
hx : f x = x
hs : MapsTo f s s
n : ℕ
⊢ x = f x

case convert_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivWithinAt f f' s x
hx : f x = x
hs : MapsTo f s s
n : ℕ
⊢ Tendsto f (𝓝[s] x) (𝓟 s)

Tactic:
exacts [hx.symm, (tendsto_principal_principal.2 hs).mono_left inf_le_right]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Box.lean
lemma existsUnique_mem_box (x : ℤ × ℤ) : ∃! n : ℕ, x ∈ box n

Proof state:
case h
x : ℤ × ℤ
⊢ (fun n => x ∈ box n) (x.1.natAbs ⊔ x.2.natAbs) ∧ ∀ (y : ℕ), (fun n => x ∈ box n) y → y = x.1.natAbs ⊔ x.2.natAbs

Tactic:
simp only [mem_box, and_self_iff, forall_eq']

Result:
no goals

Proof state:
x : ℤ × ℤ
⊢ ∃! n, x ∈ box n

Tactic:
use max x.1.natAbs x.2.natAbs

Result:
case h
x : ℤ × ℤ
⊢ (fun n => x ∈ box n) (x.1.natAbs ⊔ x.2.natAbs) ∧ ∀ (y : ℕ), (fun n => x ∈ box n) y → y = x.1.natAbs ⊔ x.2.natAbs
-- Mathlib/Data/Finsupp/ToDFinsupp.lean
theorem sigmaFinsuppEquivDFinsupp_smul {R} [Monoid R] [AddMonoid N] [DistribMulAction R N] (r : R)
    (f : (Σ i, η i) →₀ N) :
    sigmaFinsuppEquivDFinsupp (r • f) = r • sigmaFinsuppEquivDFinsupp f

Proof state:
case h.h
ι : Type u_1
η : ι → Type u_4
N : Type u_5
R : Type u_6
inst✝² : Monoid R
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction R N
r : R
f : (i : ι) × η i →₀ N
i✝ : ι
a✝ : η i✝
⊢ ((sigmaFinsuppEquivDFinsupp (r • f)) i✝) a✝ = ((r • sigmaFinsuppEquivDFinsupp f) i✝) a✝

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
R : Type u_6
inst✝² : Monoid R
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction R N
r : R
f : (i : ι) × η i →₀ N
⊢ sigmaFinsuppEquivDFinsupp (r • f) = r • sigmaFinsuppEquivDFinsupp f

Tactic:
ext

Result:
case h.h
ι : Type u_1
η : ι → Type u_4
N : Type u_5
R : Type u_6
inst✝² : Monoid R
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction R N
r : R
f : (i : ι) × η i →₀ N
i✝ : ι
a✝ : η i✝
⊢ ((sigmaFinsuppEquivDFinsupp (r • f)) i✝) a✝ = ((r • sigmaFinsuppEquivDFinsupp f) i✝) a✝
-- Mathlib/Topology/Baire/Lemmas.lean
theorem IsGδ.dense_sUnion_interior_of_closed {T : Set (Set X)} {s : Set X} (hs : IsGδ s)
    (hd : Dense s) (hc : T.Countable) (hc' : ∀ t ∈ T, IsClosed t) (hU : s ⊆ ⋃₀ T) :
    Dense (⋃ t ∈ T, interior t) :=
  hs.dense_biUnion_interior_of_closed hd hc hc' <| by rwa [← sUnion_eq_biUnion]

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
T : Set (Set X)
s : Set X
hs : IsGδ s
hd : Dense s
hc : T.Countable
hc' : ∀ t ∈ T, IsClosed t
hU : s ⊆ ⋃₀ T
⊢ s ⊆ ⋃ i ∈ T, i

Tactic:
rwa [← sUnion_eq_biUnion]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/AEMeasurable.lean
theorem MeasurableEmbedding.aemeasurable_map_iff {g : β → γ} (hf : MeasurableEmbedding f) :
    AEMeasurable g (μ.map f) ↔ AEMeasurable (g ∘ f) μ

Proof state:
case intro.intro.intro.intro
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
μ : Measure α
g : β → γ
hf : MeasurableEmbedding f
g₂ : β → γ
hgm₂ : Measurable g₂
hgm₁ : Measurable (g₂ ∘ f)
heq : g ∘ f =ᶠ[ae μ] g₂ ∘ f
⊢ AEMeasurable g (Measure.map f μ)

Tactic:
exact ⟨g₂, hgm₂, hf.ae_map_iff.2 heq⟩

Result:
no goals

Proof state:
case intro.intro
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
μ : Measure α
g : β → γ
hf : MeasurableEmbedding f
g₁ : α → γ
hgm₁ : Measurable g₁
heq : g ∘ f =ᶠ[ae μ] g₁
⊢ AEMeasurable g (Measure.map f μ)

Tactic:
rcases hf.exists_measurable_extend hgm₁ fun x => ⟨g x⟩ with ⟨g₂, hgm₂, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
μ : Measure α
g : β → γ
hf : MeasurableEmbedding f
g₂ : β → γ
hgm₂ : Measurable g₂
hgm₁ : Measurable (g₂ ∘ f)
heq : g ∘ f =ᶠ[ae μ] g₂ ∘ f
⊢ AEMeasurable g (Measure.map f μ)

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
μ : Measure α
g : β → γ
hf : MeasurableEmbedding f
⊢ AEMeasurable g (Measure.map f μ) ↔ AEMeasurable (g ∘ f) μ

Tactic:
refine ⟨fun H => H.comp_measurable hf.measurable, ?_⟩

Result:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
μ : Measure α
g : β → γ
hf : MeasurableEmbedding f
⊢ AEMeasurable (g ∘ f) μ → AEMeasurable g (Measure.map f μ)

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
μ : Measure α
g : β → γ
hf : MeasurableEmbedding f
⊢ AEMeasurable (g ∘ f) μ → AEMeasurable g (Measure.map f μ)

Tactic:
rintro ⟨g₁, hgm₁, heq⟩

Result:
case intro.intro
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
μ : Measure α
g : β → γ
hf : MeasurableEmbedding f
g₁ : α → γ
hgm₁ : Measurable g₁
heq : g ∘ f =ᶠ[ae μ] g₁
⊢ AEMeasurable g (Measure.map f μ)
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean
lemma isBigO_exp_neg_mul_of_le {c d : ℝ} (hcd : c ≤ d) :
    (fun t ↦ exp (-d * t)) =O[atTop] fun t ↦ exp (-c * t)

Proof state:
case h
c d : ℝ
hcd : c ≤ d
t : ℝ
ht : 0 < t
⊢ ‖rexp (-d * t)‖ ≤ rexp (-c * t)

Tactic:
rwa [norm_of_nonneg (exp_pos _).le, exp_le_exp, mul_le_mul_right ht, neg_le_neg_iff]

Result:
no goals

Proof state:
c d : ℝ
hcd : c ≤ d
⊢ (fun t => rexp (-d * t)) =O[atTop] fun t => rexp (-c * t)

Tactic:
apply Eventually.isBigO

Result:
case hfg
c d : ℝ
hcd : c ≤ d
⊢ ∀ᶠ (x : ℝ) in atTop, ‖rexp (-d * x)‖ ≤ rexp (-c * x)

Proof state:
case hfg
c d : ℝ
hcd : c ≤ d
⊢ ∀ᶠ (x : ℝ) in atTop, ‖rexp (-d * x)‖ ≤ rexp (-c * x)

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Result:
case h
c d : ℝ
hcd : c ≤ d
t : ℝ
ht : 0 < t
⊢ ‖rexp (-d * t)‖ ≤ rexp (-c * t)
-- Mathlib/Tactic/CategoryTheory/Bicategory/Normalize.lean
theorem evalWhiskerRight_cons_whisker
    {f : a ⟶ b} {g : a ⟶ c} {h i : b ⟶ c} {j : a ⟶ c} {k : c ⟶ d}
    {α : g ≅ f ≫ h} {η : h ⟶ i} {ηs : f ≫ i ⟶ j}
    {η₁ : h ≫ k ⟶ i ≫ k} {η₂ : f ≫ (h ≫ k) ⟶ f ≫ (i ≫ k)} {ηs₁ : (f ≫ i) ≫ k ⟶ j ≫ k}
    {ηs₂ : f ≫ (i ≫ k) ⟶ j ≫ k} {η₃ : f ≫ (h ≫ k) ⟶ j ≫ k} {η₄ : (f ≫ h) ≫ k ⟶ j ≫ k}
    {η₅ : g ≫ k ⟶ j ≫ k}
    (e_η₁ : ((Iso.refl _).hom ≫ η ≫ (Iso.refl _).hom) ▷ k = η₁) (e_η₂ : f ◁ η₁ = η₂)
    (e_ηs₁ : ηs ▷ k = ηs₁) (e_ηs₂ : (α_ _ _ _).inv ≫ ηs₁ = ηs₂)
    (e_η₃ : η₂ ≫ ηs₂ = η₃) (e_η₄ : (α_ _ _ _).hom ≫ η₃ = η₄)
    (e_η₅ : (whiskerRightIso α k).hom ≫ η₄ = η₅) :
    (α.hom ≫ (f ◁ η) ≫ ηs) ▷ k = η₅

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g : a ⟶ c
h i : b ⟶ c
j : a ⟶ c
k : c ⟶ d
α : g ≅ f ≫ h
η : h ⟶ i
ηs : f ≫ i ⟶ j
η₁ : h ≫ k ⟶ i ≫ k
η₂ : f ≫ h ≫ k ⟶ f ≫ i ≫ k
ηs₁ : (f ≫ i) ≫ k ⟶ j ≫ k
ηs₂ : f ≫ i ≫ k ⟶ j ≫ k
η₃ : f ≫ h ≫ k ⟶ j ≫ k
η₄ : (f ≫ h) ≫ k ⟶ j ≫ k
η₅ : g ≫ k ⟶ j ≫ k
e_η₁ : ((Iso.refl h).hom ≫ η ≫ (Iso.refl i).hom) ▷ k = η₁
e_η₂ : f ◁ η₁ = η₂
e_ηs₁ : ηs ▷ k = ηs₁
e_ηs₂ : (α_ f i k).inv ≫ ηs₁ = ηs₂
e_η₃ : η₂ ≫ ηs₂ = η₃
e_η₄ : (α_ f h k).hom ≫ η₃ = η₄
e_η₅ : (whiskerRightIso α k).hom ≫ η₄ = η₅
⊢ (α.hom ≫ f ◁ η ≫ ηs) ▷ k = η₅

Tactic:
simp at e_η₁ e_η₅

Result:
B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g : a ⟶ c
h i : b ⟶ c
j : a ⟶ c
k : c ⟶ d
α : g ≅ f ≫ h
η : h ⟶ i
ηs : f ≫ i ⟶ j
η₁ : h ≫ k ⟶ i ≫ k
η₂ : f ≫ h ≫ k ⟶ f ≫ i ≫ k
ηs₁ : (f ≫ i) ≫ k ⟶ j ≫ k
ηs₂ : f ≫ i ≫ k ⟶ j ≫ k
η₃ : f ≫ h ≫ k ⟶ j ≫ k
η₄ : (f ≫ h) ≫ k ⟶ j ≫ k
η₅ : g ≫ k ⟶ j ≫ k
e_η₂ : f ◁ η₁ = η₂
e_ηs₁ : ηs ▷ k = ηs₁
e_ηs₂ : (α_ f i k).inv ≫ ηs₁ = ηs₂
e_η₃ : η₂ ≫ ηs₂ = η₃
e_η₄ : (α_ f h k).hom ≫ η₃ = η₄
e_η₅ : α.hom ▷ k ≫ η₄ = η₅
e_η₁ : η ▷ k = η₁
⊢ (α.hom ≫ f ◁ η ≫ ηs) ▷ k = η₅

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g : a ⟶ c
h i : b ⟶ c
j : a ⟶ c
k : c ⟶ d
α : g ≅ f ≫ h
η : h ⟶ i
ηs : f ≫ i ⟶ j
η₁ : h ≫ k ⟶ i ≫ k
η₂ : f ≫ h ≫ k ⟶ f ≫ i ≫ k
ηs₁ : (f ≫ i) ≫ k ⟶ j ≫ k
ηs₂ : f ≫ i ≫ k ⟶ j ≫ k
η₃ : f ≫ h ≫ k ⟶ j ≫ k
η₄ : (f ≫ h) ≫ k ⟶ j ≫ k
η₅ : g ≫ k ⟶ j ≫ k
e_η₂ : f ◁ η₁ = η₂
e_ηs₁ : ηs ▷ k = ηs₁
e_ηs₂ : (α_ f i k).inv ≫ ηs₁ = ηs₂
e_η₃ : η₂ ≫ ηs₂ = η₃
e_η₄ : (α_ f h k).hom ≫ η₃ = η₄
e_η₅ : α.hom ▷ k ≫ η₄ = η₅
e_η₁ : η ▷ k = η₁
⊢ (α.hom ≫ f ◁ η ≫ ηs) ▷ k = η₅

Tactic:
simp [e_η₁, e_η₂, e_ηs₁, e_ηs₂, e_η₃, e_η₄, e_η₅]

Result:
no goals