mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
sm : MeasurableSet s
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y ↦ f y⁻¹ / ν' ((fun x ↦ x * y⁻¹) ⁻¹' s)
hg : Measurable g
⊢ μ' s * lintegral ν' g = ∫⁻ (x : G), f x ∂μ'

Tactic:
measure_mul_lintegral_eq μ' ν' sm g hg,

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
sm : MeasurableSet s
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y ↦ f y⁻¹ / ν' ((fun x ↦ x * y⁻¹) ⁻¹' s)
hg : Measurable g
⊢ ∫⁻ (x : G), ν' ((fun z ↦ z * x) ⁻¹' s) * g x⁻¹ ∂μ' = ∫⁻ (x : G), f x ∂μ'
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: case inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : a < 0
this : Tendsto (fun x ↦ (a * x + b) * x + c) atTop atBot
⊢ b * b - 4 * a * c ≤ 0

Tactic:
rcases (this.eventually (eventually_lt_atBot 0)).exists with ⟨x, hx⟩

Goal state after:
case inl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : a < 0
this : Tendsto (fun x ↦ (a * x + b) * x + c) atTop atBot
x : K
hx : (a * x + b) * x + c < 0
⊢ b * b - 4 * a * c ≤ 0
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ ν : Measure α
inst✝ : ENorm ε
f : α → ε
hμ : ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
hν : ∫⁻ (a : α), ‖f a‖ₑ ∂ν < ∞
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ + ∫⁻ (a : α), ‖f a‖ₑ ∂ν < ∞

Tactic:
exact add_lt_top.2 ⟨hμ, hν⟩

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: a : ℕ
⊢ 0 ≤ a.sqrt + 1

Tactic:
· exact Nat.le_add_left 0 (Nat.sqrt a + 1)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (μ.withDensity f).prod ν = (μ.prod ν).withDensity fun z ↦ f z.1

Tactic:
refine ext_of_lintegral _ fun φ hφ ↦ ?_
  rw [lintegral_prod _ hφ.aemeasurable, lintegral_withDensity_eq_lintegral_mul₀ hf,
    lintegral_withDensity_eq_lintegral_mul₀ _ hφ.aemeasurable, lintegral_prod]
  · refine lintegral_congr (fun x ↦ ?_)
    rw [Pi.mul_apply, ← lintegral_const_mul'' _ (by fun_prop)]
    simp
  all_goals fun_prop (disch := intro _ hs; simp [hs])

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: case inl
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module ℚ≥0 M
inst✝⁴ : AddCommMonoid N
inst✝³ : PartialOrder N
inst✝² : IsOrderedAddMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
p : M → Prop
f : ι → M
h_zero : m 0 = 0
h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b
hp_add : ∀ (a b : M), p a → p b → p (a + b)
h_div : ∀ (n : ℕ) (a : M), p a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs : ∀ i ∈ ∅, p (f i)
⊢ m (𝔼 i ∈ ∅, f i) ≤ 𝔼 i ∈ ∅, m (f i)

Tactic:
simp [h_zero]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ x * x⋆ ≠ 0 ↔ x ≠ 0

Tactic:
simp only [Ne, mul_star_self_eq_zero_iff]

Goal state after:
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: 𝕜 : Type u_2
𝕜' : Type u_3
inst✝¹ : RCLike 𝕜
inst✝ : RCLike 𝕜'
h : RCLike.im RCLike.I = 1
a : 𝕜
⊢ 0 ≤ (RCLike.map 𝕜 𝕜') a ↔ 0 ≤ a

Tactic:
RCLike.nonneg_iff,

Goal state after:
𝕜 : Type u_2
𝕜' : Type u_3
inst✝¹ : RCLike 𝕜
inst✝ : RCLike 𝕜'
h : RCLike.im RCLike.I = 1
a : 𝕜
⊢ 0 ≤ RCLike.re ((RCLike.map 𝕜 𝕜') a) ∧ RCLike.im ((RCLike.map 𝕜 𝕜') a) = 0 ↔ 0 ≤ a
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: r : ℝ
⊢ 2⁻¹ • (↑r + star ↑r) = ↑r

Tactic:
star_def,

Goal state after:
r : ℝ
⊢ 2⁻¹ • (↑r + (starRingEnd ℂ) ↑r) = ↑r
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
n : ℕ
⊢ ‖↑n‖ = ↑n

Tactic:
rw [← ofReal_natCast]
  exact norm_of_nonneg (Nat.cast_nonneg n)

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Z → X
x : Z
h : f ⁻¹' e.source ∈ 𝓝 x
hx : f x ∈ e.source
⊢ ContinuousAt f x ↔ ContinuousAt (↑e ∘ f) x

Tactic:
have h' : f ⁻¹' e.source ∈ 𝓝[univ] x := by rwa [nhdsWithin_univ]

Goal state after:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Z → X
x : Z
h : f ⁻¹' e.source ∈ 𝓝 x
hx : f x ∈ e.source
h' : f ⁻¹' e.source ∈ 𝓝[univ] x
⊢ ContinuousAt f x ↔ ContinuousAt (↑e ∘ f) x
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
f' : α → E'
l : Filter α
h : ∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0
⊢ ¬f' =o[l] f'

Tactic:
intro ho

Goal state after:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
f' : α → E'
l : Filter α
h : ∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0
ho : f' =o[l] f'
⊢ False
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
G' : Type u_8
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : SeminormedAddCommGroup G'
c : ℝ
f' : α → E'
g' : α → F'
k' : α → G'
l : Filter α
hf : IsBigOWith c l f' k'
hg : IsBigOWith c l g' k'
⊢ IsBigOWith c l (fun x ↦ (f' x, g' x)) k'

Tactic:
by
  rw [isBigOWith_iff] at *; filter_upwards [hf, hg] with x using max_le

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case inl
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
B : ι → α → ℝ
hAB : ∀ i ∈ ∅, IsBigOWith (C i) l (A i) (B i)
⊢ IsBigOWith (sSup (C '' ↑∅)) l (fun H ↦ ∑ i ∈ ∅, A i H) fun H ↦ ∑ i ∈ ∅, ‖B i H‖

pp: case inr
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hAB : ∀ i ∈ s, IsBigOWith (C i) l (A i) (B i)
hs : s.Nonempty
⊢ IsBigOWith (sSup (C '' ↑s)) l (fun H ↦ ∑ i ∈ s, A i H) fun H ↦ ∑ i ∈ s, ‖B i H‖

Tactic:
· simp [isBigOWith_zero]

Goal state after:
case inr
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hAB : ∀ i ∈ s, IsBigOWith (C i) l (A i) (B i)
hs : s.Nonempty
⊢ IsBigOWith (sSup (C '' ↑s)) l (fun H ↦ ∑ i ∈ s, A i H) fun H ↦ ∑ i ∈ s, ‖B i H‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case e_a
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
⊢ ∑ i ∈ s, ‖B i x‖ = ‖∑ i ∈ s, ‖B i x‖‖

Tactic:
rw [Real.norm_of_nonneg (Finset.sum_nonneg (fun _ _ ↦ norm_nonneg _))]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case e_a
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
C : ℝ
i : α → Finset ι
hAB : ∀ᶠ (x : ι × α) in ⊤ ×ˢ l, ‖Function.uncurry A x‖ ≤ C * ‖Function.uncurry B x‖
s₁ : ι → Prop
hs₁ : ∀ᶠ (x : ι) in ⊤, s₁ x
s₂ : α → Prop
hs₂ : ∀ᶠ (y : α) in l, s₂ y
hbound : ∀ {x : ι}, s₁ x → ∀ {y : α}, s₂ y → ‖Function.uncurry A (x, y)‖ ≤ C * ‖Function.uncurry B (x, y)‖
H : α
hH : s₂ H
⊢ ∑ j ∈ i H, ‖B j H‖ = ‖∑ j ∈ i H, ‖B j H‖‖

Tactic:
rw [Real.norm_of_nonneg (Finset.sum_nonneg (fun _ _ ↦ norm_nonneg _))]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
l✝ : Filter α
ι : Type u_17
R : Type u_18
𝕜 : Type u_19
inst✝¹ : SeminormedCommRing R
inst✝ : NormedField 𝕜
f : ι → α → R
g : ι → α → 𝕜
l : List ι
hf : ∀ i ∈ ↑l, f i =O[l✝] g i
⊢ (fun x ↦ (Multiset.map (fun x_1 ↦ f x_1 x) ↑l).prod) =O[l✝] fun x ↦ (Multiset.map (fun x_1 ↦ g x_1 x) ↑l).prod

Tactic:
exact mod_cast IsBigO.listProd hf

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ sin ((starRingEnd ℂ) x) / cos ((starRingEnd ℂ) x) = (starRingEnd ℂ) (tan x)

Tactic:
sin_conj,

Goal state after:
x : ℂ
⊢ (starRingEnd ℂ) (sin x) / cos ((starRingEnd ℂ) x) = (starRingEnd ℂ) (tan x)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cos ((starRingEnd ℂ) x) / sin ((starRingEnd ℂ) x) = (starRingEnd ℂ) x.cot

Tactic:
sin_conj,

Goal state after:
x : ℂ
⊢ cos ((starRingEnd ℂ) x) / (starRingEnd ℂ) (sin x) = (starRingEnd ℂ) x.cot
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℝ
⊢ cosh (x + y) = cosh x * cosh y + sinh x * sinh y

Tactic:
by
  rw [← ofReal_inj]; simp [cosh_add]

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x r : ℝ
⊢ expNear 0 x r = r

Tactic:
by simp [expNear]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: case inr
n : ℕ
hn : 0 < n
⊢ (fun x ↦ cexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !) =O[𝓝 0] fun x ↦ x ^ n

Tactic:
refine .of_bound (n.succ / (n ! * n)) ?_

Goal state after:
case inr
n : ℕ
hn : 0 < n
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, ‖cexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !‖ ≤ ↑n.succ / (↑n ! * ↑n) * ‖x ^ n‖
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ
⊢ Tendsto f l (comap rexp (𝓝 0)) ↔ Tendsto f l atBot

Tactic:
comap_exp_nhds_zero

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: k : ℕ
r : ℝ
hr : 0 < r
⊢ rexp (-r) < 1

Tactic:
exp_lt_one_iff,

Goal state after:
k : ℕ
r : ℝ
hr : 0 < r
⊢ -r < 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case inl
x : ℝ
hx₁ : -π < x
hx₂ : x < π
h : x ≠ 0
h0 : x < 0
⊢ sin x ≠ 0

Tactic:
| inl h0 =>

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ (range sin).Infinite

Tactic:
rw [Real.range_sin]

Goal state after:
⊢ (Icc (-1) 1).Infinite
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁸ : SeminormedAddCommGroup M
inst✝⁷ : SeminormedAddCommGroup N
R : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : Module R M
S T : Submodule R M
𝕜 : Type u_4
inst✝⁴ : SeminormedCommRing 𝕜
inst✝³ : Module 𝕜 M
inst✝² : IsBoundedSMul 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
k : 𝕜
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
a : M
h : ∀ (x : ℝ), x - ‖mk a‖ < δ ∧ ‖mk a‖ - x < δ → ‖k‖ * x - ‖k‖ * ‖mk a‖ < ε ∧ ‖k‖ * ‖mk a‖ - ‖k‖ * x < ε
ha : ‖a‖ < ‖mk a‖ + δ
⊢ ‖mk a‖ - ‖a‖ < δ

Tactic:
linarith [Submodule.Quotient.norm_mk_le S a]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : 0 < r
⊢ interior (closedBall x r) ⊆ ball x r

Tactic:
intro y hy

Goal state after:
case inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : 0 < r
y : E
hy : y ∈ interior (closedBall x r)
⊢ y ∈ ball x r
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
hr : r ∈ closedBall 0 (ε / R)
⊢ (fun x_1 ↦ -x + x_1) ⁻¹' (r • s) ⊆ u

Tactic:
intro y hy

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
hr : r ∈ closedBall 0 (ε / R)
y : E
hy : y ∈ (fun x_1 ↦ -x + x_1) ⁻¹' (r • s)
⊢ y ∈ u
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ 2 * s * c * c + cos (2 * θ) * s = 2 * s * c * c + (2 * c ^ 2 - 1) * s

Tactic:
by rw [cos_two_mul]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
⊢ ∃ y, dist x y ≤ δ ∧ dist y z ≤ ε

Tactic:
obtain rfl | hε' := hε.eq_or_lt
  · exact ⟨z, by rwa [zero_add] at h, (dist_self _).le⟩
  have hεδ := add_pos_of_pos_of_nonneg hε' hδ
  refine (exists_dist_eq x z (div_nonneg hε <| add_nonneg hε hδ)
    (div_nonneg hδ <| add_nonneg hε hδ) <| by
      rw [← add_div, div_self hεδ.ne']).imp
    fun y hy => ?_
  rw [hy.1, hy.2, div_mul_comm, div_mul_comm ε]
  rw [← div_le_one hεδ] at h
  exact ⟨mul_le_of_le_one_left hδ h, mul_le_of_le_one_left hε h⟩

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case left
c : ℝ := ⋯
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / (2 * 4)
⊢ -(π / 2) ≤ π / 5

Tactic:
linarith [pi_pos.le]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case right
c : ℝ := ⋯
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / (2 * 4)
⊢ π / 5 ≤ π / 2

Tactic:
linarith [pi_pos.le]

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ ∑' (i : ℕ), x ^ (i + 1) = ∑' (i : ℕ), x ^ i - 1

Tactic:
eq_sub_iff_add_eq,

Goal state after:
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ ∑' (i : ℕ), x ^ (i + 1) + 1 = ∑' (i : ℕ), x ^ i
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactPair Y Z
⊢ ∀ (x : C(X, Y) × C(Y, Z)), Tendsto (fun x ↦ x.2.comp x.1) (𝓝 x) (𝓝 (x.2.comp x.1))

Tactic:
tendsto_nhds_compactOpen

Goal state after:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactPair Y Z
⊢ ∀ (x : C(X, Y) × C(Y, Z)) (K : Set X),
    IsCompact K →
      ∀ (U : Set Z),
        IsOpen[inst✝¹] U →
          MapsTo (⇑(x.2.comp x.1)) K U → ∀ᶠ (a : C(X, Y) × C(Y, Z)) in 𝓝 x, MapsTo (⇑(a.2.comp a.1)) K U
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace T
K : Set X
U : Set Y
inst✝ : RegularSpace Y
f : C(X, Y)
⊢ Tendsto id ((𝓝 f).lift' closure) (𝓝 f)

Tactic:
tendsto_nhds_compactOpen

Goal state after:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace T
K : Set X
U : Set Y
inst✝ : RegularSpace Y
f : C(X, Y)
⊢ ∀ (K : Set X),
    IsCompact K →
      ∀ (U : Set Y), IsOpen[inst✝³] U → MapsTo (⇑f) K U → ∀ᶠ (a : C(X, Y)) in (𝓝 f).lift' closure, MapsTo (⇑(id a)) K U
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ IsPathConnected (pathComponent x)

Tactic:
rw [← pathComponentIn_univ]
  exact isPathConnected_pathComponentIn (mem_univ x)

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i • z i

Tactic:
rw [← cauchySeq_shift 1]

Goal state after:
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n ↦ ∑ i ∈ Finset.range (n + 1), f i • z i
Module: Mathlib.Topology.Instances.Sign

Goal state before:
pp: α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableLT α
inst✝ : OrderTopology α
a : α
h : a < 0
⊢ ContinuousAt (⇑SignType.sign) a

Tactic:
by
  refine (continuousAt_const : ContinuousAt (fun x => (-1 : SignType)) a).congr ?_
  rw [Filter.EventuallyEq, eventually_nhds_iff]
  exact ⟨{ x | x < 0 }, fun x hx => (sign_neg hx).symm, isOpen_gt' 0, h⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
hx : |p| * ‖↑(p⁻¹ * x)‖ = ‖↑x‖
⊢ ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|

Tactic:
← hx,

Goal state after:
case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
hx : |p| * ‖↑(p⁻¹ * x)‖ = ‖↑x‖
⊢ |p| * ‖↑(p⁻¹ * x)‖ = |x - ↑(round (p⁻¹ * x)) * p|
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case refine_1
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n ↦ ∑ i ∈ Finset.range n, b * |f (i + 1) - f i|

pp: case refine_2
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b
n : ℕ
⊢ ‖(f (n + 1) + -f n) • (Finset.range (n + 1)).sum z‖ ≤ b * |f (n + 1) - f n|

Tactic:
· simp_rw [abs_of_nonneg (sub_nonneg_of_le (hfa (Nat.le_succ _))), ← mul_sum]
    apply Real.uniformContinuous_const_mul.comp_cauchySeq
    simp_rw [sum_range_sub, sub_eq_add_neg]
    exact (Tendsto.cauchySeq hf0).add_const

Goal state after:
case refine_2
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b
n : ℕ
⊢ ‖(f (n + 1) + -f n) • (Finset.range (n + 1)).sum z‖ ≤ b * |f (n + 1) - f n|
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
⊢ ContinuousAt log x ↔ x ≠ 0

Tactic:
by
  refine ⟨?_, continuousAt_log⟩
  rintro h rfl
  exact not_tendsto_nhds_of_tendsto_atBot tendsto_log_nhdsNE_zero _ <|
    h.tendsto.mono_left nhdsWithin_le_nhds

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x : ℂ
⊢ x ^ 0 = 1

Tactic:
by simp [cpow_def]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
⊢ x⁻¹.arg = if x.arg = π then π else -x.arg

Tactic:
← arg_conj,

Goal state after:
x : ℂ
⊢ x⁻¹.arg = ((starRingEnd ℂ) x).arg
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr
ψ : Angle
⊢ |(ψ + ↑π).cos| = |ψ.cos|

Tactic:
cos_add_pi,

Goal state after:
case inr
ψ : Angle
⊢ |(-ψ.cos)| = |ψ.cos|
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case neg
x y : ℝ
hx : ¬x = 0
⊢ |x| ^ y ≤ rexp (log x * y)

Tactic:
rw [rpow_def_of_pos (abs_pos.2 hx), log_abs]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ x ^ z < y ^ z

Tactic:
← hx,

Goal state after:
case inl
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ 0 ^ z < y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: ι : Type u_1
s : Multiset ι
f : ι → ℝ
hs : ∀ i ∈ s, 0 ≤ f i
r : ℝ
⊢ (Multiset.map (fun x ↦ f x ^ r) s).prod = (Multiset.map f s).prod ^ r

Tactic:
obtain ⟨l⟩ := s
  simpa using Real.list_prod_map_rpow' l f hs r

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ x ^ (-z) ≤ y ^ (-z)

pp: case hx
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ y

pp: case hx
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ x

pp: case ha
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 < x ^ z

pp: case hb
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 < y ^ z

Tactic:
on_goal 1 => refine rpow_le_rpow ?_ hxy (neg_nonneg.2 hz)

Goal state after:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ x

case hx
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ y

case hx
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ x

case ha
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 < x ^ z

case hb
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 < y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: p : ℝ × ℝ
hp : p.1 < 0 ∨ 0 < p.1
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) p

Tactic:
cases hp with

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top
y : ℝ
⊢ ∞ ^ y = 0 ↔ ∞ = 0 ∧ 0 < y ∨ ∞ = ∞ ∧ y < 0

Tactic:
rcases lt_trichotomy y 0 with (H | H | H) <;>
      simp [H, top_rpow_of_neg, top_rpow_of_pos, le_of_lt]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 < x
⊢ rexp (log x * y) < 1 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y

Tactic:
exp_lt_one_iff,

Goal state after:
x y : ℝ
hx : 0 < x
⊢ log x * y < 0 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top
y : ℝ
⊢ ∞ ^ y = ∞ ↔ ∞ = 0 ∧ y < 0 ∨ ∞ = ∞ ∧ 0 < y

Tactic:
rcases lt_trichotomy y 0 with (H | H | H) <;>
      simp [H, top_rpow_of_neg, top_rpow_of_pos, le_of_lt]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x ≠ 0
y : ℝ
hy : y ∈ {y | 0 ≤ y}
z : ℝ
hz : z ∈ {y | 0 ≤ y}
hyz : y ^ x = z ^ x
⊢ y ^ 1 = z ^ 1

Tactic:
← mul_inv_cancel₀ hx,

Goal state after:
x : ℝ
hx : x ≠ 0
y : ℝ
hy : y ∈ {y | 0 ≤ y}
z : ℝ
hz : z ∈ {y | 0 ≤ y}
hyz : y ^ x = z ^ x
⊢ y ^ (x * x⁻¹) = z ^ (x * x⁻¹)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inl
x : ℝ≥0∞
⊢ x⁻¹ ^ 0 = (x ^ 0)⁻¹

pp: case inr
x : ℝ≥0∞
y : ℝ
hy : y ≠ 0
⊢ x⁻¹ ^ y = (x ^ y)⁻¹

Tactic:
· simp only [rpow_zero, inv_one]

Goal state after:
case inr
x : ℝ≥0∞
y : ℝ
hy : y ≠ 0
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: b : ℝ
hb : 1 < b
⊢ StrictMono fun x ↦ b ^ x

Tactic:
by
  simp_rw [Real.rpow_def_of_pos (zero_lt_one.trans hb)]
  exact exp_strictMono.comp <| StrictMono.const_mul strictMono_id <| Real.log_pos hb

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ StrictAnti fun x ↦ b ^ x

Tactic:
simp_rw [Real.rpow_def_of_pos hb₀]

Goal state after:
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ StrictAnti fun x ↦ rexp (log b * x)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p = 0
⊢ 0 < x ^ p

pp: case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : ¬p = 0
⊢ 0 < x ^ p

Tactic:
· simp [hp_zero, zero_lt_one]

Goal state after:
case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : ¬p = 0
⊢ 0 < x ^ p