mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (f * g) a ∂μ = ∫⁻ (a : α) in s, g a ∂μ.withDensity f

Tactic:
restrict_withDensity hs,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (f * g) a ∂μ = ∫⁻ (a : α), g a ∂(μ.restrict s).withDensity f
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: p : ℝ × ℝ
⊢ equivRealProd.symm p = ↑p.1 + ↑p.2 * I

Tactic:
by
  ext <;> simp [Complex.equivRealProd, ofReal]

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

Goal state before:
pp: ⊢ I⁻¹ = -I

Tactic:
by
  rw [inv_eq_one_div, div_I, one_mul]

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

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x y : V₁
⊢ ‖f (x - y)‖ ≤ ↑⟨‖f‖, ⋯⟩ * ‖x - y‖

Tactic:
apply le_opNorm

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

Goal state before:
pp: case h₁
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ f g : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖f v‖ ≤ ‖f‖ * ‖v‖

Tactic:
apply le_opNorm

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

Goal state before:
pp: case h₂
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ f g : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖g v‖ ≤ ‖g‖ * ‖v‖

Tactic:
apply le_opNorm

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

Goal state before:
pp: case hbc
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
f : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖f v‖ ≤ ‖f‖ * ‖v‖

Tactic:
apply le_opNorm

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : StarMul G
a b : G
⊢ (star b)⁻¹ * star a * (a * b⁻¹) = 1 ↔ star a * a = star b * b

Tactic:
mul_assoc,

Goal state after:
G : Type u_2
inst✝¹ : Group G
inst✝ : StarMul G
a b : G
⊢ (star b)⁻¹ * (star a * (a * b⁻¹)) = 1 ↔ star a * a = star b * b
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: E : Type u_2
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CStarRing E
inst✝ : Nontrivial E
⊢ ‖1‖ = 1

Tactic:
have : 0 < ‖(1 : E)‖ := norm_pos_iff.mpr one_ne_zero
  rw [← mul_left_inj' this.ne', ← norm_star_mul_self, mul_one, star_one, one_mul]

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

Goal state before:
pp: case succ
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ (‖x‖₊ ^ 2 ^ k) ^ 2 = ‖x‖₊ ^ (2 * 2 ^ k)

Tactic:
pow_mul'

Goal state after:
case succ
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ (‖x‖₊ ^ 2 ^ k) ^ 2 = (‖x‖₊ ^ 2 ^ k) ^ 2
Module: Mathlib.Topology.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃A[R] B
S : Set B
⊢ ⇑e.symm.symm ⁻¹' S = ⇑e ⁻¹' S

Tactic:
e.symm_symm

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃A[R] B
S : Set B
⊢ ⇑e ⁻¹' S = ⇑e ⁻¹' S
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: x : ℂ
⊢ restrictScalars ℝ (toSpanSingleton ℂ x) = x • 1

Tactic:
by
  ext1 z
  dsimp
  apply mul_comm

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

Goal state before:
pp: f : ℝ →+* ℂ
h : Continuous ⇑f
⊢ f = ofRealHom

Tactic:
convert!
    congr_arg AlgHom.toRingHom <|
      Subsingleton.elim (AlgHom.mk' f <| map_real_smul f h) (Algebra.ofId ℝ ℂ)

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

Goal state before:
pp: z : ℝ
hz : 0 ≤ ↑z
⊢ ↑z = ↑‖↑z‖

Tactic:
rw [norm_real, Real.norm_of_nonneg (id hz.1 : 0 ≤ z)]

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(ℑ (I • a)) = ↑(ℜ a)

Tactic:
simp [realPart_apply_coe, imaginaryPart_apply_coe, smul_comm I (2⁻¹ : ℝ), smul_smul I]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
r : ℝ
⊢ re (z / ↑r) = re z / r

Tactic:
by
  rw [div_eq_inv_mul, div_eq_inv_mul, ← ofReal_inv, re_ofReal_mul]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ ‖(starRingEnd K) z‖ₑ = ‖z‖ₑ

Tactic:
by simp [enorm]

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
t : Set Y
hs : t ⊆ e.target
⊢ IsOpen[inst✝¹] (↑e.symm '' t) ↔ IsOpen[inst✝] t

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ e.symm.isOpen_image_of_subset_source h hs⟩
  have hs' : e.symm '' t ⊆ e.source := by
    rw [e.symm_image_eq_source_inter_preimage hs]
    apply Set.inter_subset_left
  rw [← e.image_symm_image_of_subset_target hs]
  exact e.isOpen_image_of_subset_source h hs'

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
hs : s ⊆ e.source
⊢ IsOpen[inst✝] (↑e '' s) ↔ IsOpen[inst✝] (↑e.symm.symm '' s)

Tactic:
e.symm_symm

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
hs : s ⊆ e.source
⊢ IsOpen[inst✝] (↑e '' s) ↔ IsOpen[inst✝] (↑e '' s)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : ℝ
⊢ ↑0 ≤ ↑x ↔ 0 ≤ x

Tactic:
ofReal_le_ofReal

Goal state after:
K : Type u_1
inst✝ : RCLike K
x : ℝ
⊢ 0 ≤ x ↔ 0 ≤ x
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : ℝ
⊢ ↑x ≤ ↑0 ↔ x ≤ 0

Tactic:
ofReal_le_ofReal

Goal state after:
K : Type u_1
inst✝ : RCLike K
x : ℝ
⊢ x ≤ 0 ↔ x ≤ 0
Module: Mathlib.Analysis.Asymptotics.Theta

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
⊢ f =Θ[⊥] g

Tactic:
by simp [IsTheta]

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

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (fun x ↦ ‖f' x‖) =Θ[l] g ↔ f' =Θ[l] g

Tactic:
by simp [IsTheta]

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (f =Θ[l] fun x ↦ ‖g' x‖) ↔ f =Θ[l] g'

Tactic:
by simp [IsTheta]

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : f₁ =O[l] g₁
h₂ : f₂ =O[l] g₂
c₁ : ℝ
hc₁ : IsBigOWith c₁ l f₁ g₁
c₂ : ℝ
hc₂ : IsBigOWith c₂ l f₂ g₂
⊢ (fun x ↦ f₁ x + f₂ x) =O[l] fun x ↦ ‖g₁ x‖ + ‖g₂ x‖

Tactic:
exact (hc₁.add_add hc₂).isBigO

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

Goal state before:
pp: F : Type u_4
inst✝⁴ : Norm F
α : Type u_17
E : Type u_18
inst✝³ : NormedRing E
inst✝² : One F
inst✝¹ : NormOneClass F
inst✝ : TopologicalSpace α
f : α → E
x : α
⊢ ContinuousAt f x ↔ (fun x_1 ↦ f x_1 - f x) =o[𝓝 x] fun x ↦ 1

Tactic:
simp [ContinuousAt, ← tendsto_sub_nhds_zero_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
h₂ : (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k
h₃ :
  ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k
two_mul_two : 4 = 2 * 2
hQ0 : Q ≠ 0
h2Q0 : 2 * Q ≠ 0
⊢ ε / 2 + ε / (2 * 2 * Q) * (2 * Q) = ε

Tactic:
mul_assoc,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
h₂ : (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k
h₃ :
  ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k
two_mul_two : 4 = 2 * 2
hQ0 : Q ≠ 0
h2Q0 : 2 * Q ≠ 0
⊢ ε / 2 + ε / (2 * (2 * Q)) * (2 * Q) = ε
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
⊢ 1 < rexp x ↔ 0 < x

Tactic:
by rw [← exp_zero, exp_lt_exp]

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

Goal state before:
pp: x : ℝ
⊢ rexp x < 1 ↔ x < 0

Tactic:
by rw [← exp_zero, exp_lt_exp]

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

Goal state before:
pp: x : ℂ
⊢ cexp (x * I) - cexp (-(x * I)) = (cexp (-x * I) - cexp (x * I)) * I * I

Tactic:
mul_assoc,

Goal state after:
x : ℂ
⊢ cexp (x * I) - cexp (-(x * I)) = (cexp (-x * I) - cexp (x * I)) * (I * I)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ sinh (x * I + y * I) = sinh (x * I) * cos y + cos x * sin y * I

Tactic:
mul_assoc,

Goal state after:
x y : ℂ
⊢ sinh (x * I + y * I) = sinh (x * I) * cos y + cos x * (sin y * I)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
n : ℕ
h : 1 < n
this : (fun x ↦ ‖x‖ ^ n) =o[𝓝 0] fun x ↦ ‖x‖ ^ 1
⊢ (fun x ↦ ‖x‖ ^ n) =o[𝓝 0] fun x ↦ x

Tactic:
simp only [pow_one] at this

Goal state after:
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
n : ℕ
h : 1 < n
this : (fun x ↦ ‖x‖ ^ n) =o[𝓝 0] fun x ↦ ‖x‖
⊢ (fun x ↦ ‖x‖ ^ n) =o[𝓝 0] fun x ↦ x
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cosh (3 * x * I) = 4 * cos x ^ 3 - 3 * cos x

Tactic:
mul_assoc,

Goal state after:
x : ℂ
⊢ cosh (3 * (x * I)) = 4 * cos x ^ 3 - 3 * cos x
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : |x| = x
h4 : |x| ≤ 1
h' : |rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial| ≤ |x| ^ n * (↑n.succ / (↑n.factorial * ↑n))
⊢ rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n + 1) / (↑n.factorial * ↑n)

Tactic:
rw [h3] at h'

Goal state after:
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : |x| = x
h4 : |x| ≤ 1
h' : |rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial| ≤ x ^ n * (↑n.succ / (↑n.factorial * ↑n))
⊢ rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n + 1) / (↑n.factorial * ↑n)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h : ∀ᶠ (n : ℕ) in atTop, g n = 0 → f n = 0
hrec :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
⊢ f =O[atTop] g

Tactic:
rw [← eventually_forall_ge_atTop] at h
  obtain ⟨n₀, h, hrec⟩ := h.and hrec |>.exists
  obtain ⟨C₀, hrec⟩ := hrec
  rw [isBigO_iff]
  rw [← eventually_forall_ge_atTop] at hrec
  obtain ⟨n₁, H₁, H₂⟩ := (eventually_ge_atTop n₀).and hrec |>.exists
  let ubounds := {C | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
  let C₁ := (Finset.Icc n₀ n₁).sup' (Finset.nonempty_Icc.mpr H₁) fun n => ‖f n‖ / ‖g n‖
  have C₁_mem : C₁ ∈ ubounds := by
    rw [Set.mem_ofPred]
    intro m hm
    calc ‖f m‖ = (‖f m‖ / ‖g m‖) * ‖g m‖ := by by_cases hm' : g m = 0 <;> grind [norm_eq_zero]
      _ ≤ C₁ * ‖g m‖ := by
        gcongr
        exact Finset.le_sup' (fun x => ‖f x‖ / ‖g x‖) (Finset.mem_def.mpr hm)
  refine ⟨max C₀ C₁, ?_⟩
  filter_upwards [eventually_ge_atTop n₁] with n hn
  induction n using Nat.strongRecOn with
  | ind n h_ind =>
    refine H₂ _ (by grind) _ (by grind) fun m hm => ?_
    by_cases hbase : m < n₁
    · have hC₁ : C₁ ≤ max C₀ C₁ := by grind
      grw [← hC₁]
      grind
    · grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) →
      ∀ (m : ℕ), n.succ ≤ m → m = k + n.succ → abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
kn : k + n.succ ≥ n.succ
⊢ abv (f (k + n.succ).succ) ≤ ?m.259 * r

Tactic:
by rw [mul_comm] <;> exact h _ (Nat.le_of_succ_le kn)

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x✝ : M ⧸ S
m : M
r✝ ε : ℝ
x : M ⧸ S
r : ℝ
⊢ r ≤ infDist 1 {m | ↑m = x⁻¹} ↔ r ≤ infDist 1 {m | ↑m = x}

Tactic:
by
    simp only [le_infDist (norm_aux _)]
    exact (Equiv.inv _).forall_congr (by simp [← inv_eq_iff_eq_inv])

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

Goal state before:
pp: x : ℝ
h : cos x = 1
n : ℤ
hn : ↑(n / 2) * ↑2 * π + π = x
hn1 : n % 2 = 1
⊢ ↑(n / 2) * (2 * π) = x

Tactic:
mul_assoc,

Goal state after:
x : ℝ
h : cos x = 1
n : ℤ
hn : ↑(n / 2) * (↑2 * π) + π = x
hn1 : n % 2 = 1
⊢ ↑(n / 2) * (2 * π) = x
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedGroup E
s t : Set E
hst : IsBounded (s * t)
⊢ IsBounded s ∨ IsBounded t

Tactic:
by
  symm
  exact AntilipschitzWith.isBounded_of_image2_left _ (fun x => (isometry_mul_left x).antilipschitz)
    (by rwa [image2_swap])

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure ≠ univ
⊢ ∃ x, 0 < ‖↑x‖

Tactic:
by
    refine (Set.nonempty_compl.2 h).imp fun x hx ↦ ?_
    exact (norm_nonneg _).lt_of_ne' <| mt norm_mk_eq_zero_iff_mem_closure.1 hx

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

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c ↦ c • (y - x) + x
c : ℝ
hc : c ∈ f ⁻¹' closedBall x (dist y x)
⊢ ‖c‖ ≤ 1

Tactic:
← mul_le_mul_iff_left₀ hr

Goal state after:
case inr.inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c ↦ c • (y - x) + x
c : ℝ
hc : c ∈ f ⁻¹' closedBall x (dist y x)
⊢ ‖c‖ * dist y x ≤ 1 * dist y x
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n ↦ ↑((n + k).choose k) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
I1 : Summable fun n ↦ ‖↑((n + k).choose k) * r ^ n‖
n i : ℕ
hi : i < n + 1
⊢ ↑((i + k).choose k) * r ^ i * r ^ (n - i) = ↑((i + k).choose k) * r ^ n

Tactic:
mul_assoc,

Goal state after:
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n ↦ ↑((n + k).choose k) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
I1 : Summable fun n ↦ ‖↑((n + k).choose k) * r ^ n‖
n i : ℕ
hi : i < n + 1
⊢ ↑((i + k).choose k) * (r ^ i * r ^ (n - i)) = ↑((i + k).choose k) * r ^ n
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
⊢ Summable fun b ↦ ∑ i ∈ Finset.range k, ↑(a i) * ↑b ^ i * r ^ b

Tactic:
apply summable_sum (fun i hi ↦ ?_)

Goal state after:
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
a : ℕ → ℕ
ha : ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
i : ℕ
hi : i ∈ Finset.range k
⊢ Summable fun b ↦ ↑(a i) * ↑b ^ i * r ^ b
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case neg
α : Type u_1
inst✝ : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n ↦ if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ n ≥ N, u n = v n
n : ℕ
H : ¬n < N
⊢ ‖u n‖ ≤ C * r ^ n

Tactic:
· push Not at H
    exact h _ H

Goal state after:
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)
⊢ (𝓝 f).lift' closure ≤ 𝓝 f

Tactic:
by
    rw [← tendsto_id', tendsto_nhds_compactOpen]
    intro K hK U hU hf
    rcases (hK.image f.continuous).exists_isOpen_closure_subset (hU.mem_nhdsSet.2 hf.image_subset)
      with ⟨V, hVo, hKV, hVU⟩
    filter_upwards [mem_lift' (eventually_mapsTo hK hVo (mapsTo_iff_image_subset.2 hKV))] with g hg
    refine ((isClosed_setOfPred_mapsTo isClosed_closure K).closure_subset ?_).mono_right hVU
    exact closure_mono (fun _ h ↦ h.mono_right subset_closure) hg

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
γ : Path x y
γ' : Path y z
f : X → Y
h : Continuous[inst✝¹, inst✝] f
⊢ (γ.trans γ').map h = (γ.map h).trans (γ'.map h)

Tactic:
ext t
  rw [trans_apply, map_coe, Function.comp_apply, trans_apply, map_coe, map_coe]
  grind

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

Goal state before:
pp: p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
⊢ p * 1 ≤ p * ↑(addOrderOf u) * (↑n / ↑(addOrderOf u))

Tactic:
mul_assoc,

Goal state after:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
⊢ p * 1 ≤ p * (↑(addOrderOf u) * (↑n / ↑(addOrderOf u)))
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case pos
x : ℝ
hx0 : x ≤ 0
⊢ rexp 1 * x ≤ rexp x

pp: case neg
x : ℝ
hx0 : ¬x ≤ 0
⊢ rexp 1 * x ≤ rexp x

Tactic:
· apply le_trans (mul_nonpos_of_nonneg_of_nonpos (exp_pos 1).le hx0) (exp_nonneg x)

Goal state after:
case neg
x : ℝ
hx0 : ¬x ≤ 0
⊢ rexp 1 * x ≤ rexp x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
⊢ -π < (log x).im

Tactic:
by simp only [log_im, neg_pi_lt_arg]

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

Goal state before:
pp: ⊢ 2 • ↑(-π / 2) = ↑π

Tactic:
by
  rw [two_nsmul_coe_div_two, coe_neg, neg_coe_pi]

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

Goal state before:
pp: case mp.inl
θ ψ : ℝ
n : ℤ
hn : ↑n * π * 2 - ψ = θ
⊢ ↑(↑n * π * 2) = 0

Tactic:
mul_assoc,

Goal state after:
case mp.inl
θ ψ : ℝ
n : ℤ
hn : ↑n * π * 2 - ψ = θ
⊢ ↑(↑n * (π * 2)) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp.inr
θ ψ : ℝ
n : ℤ
hn : ↑n * π * 2 + ψ = θ
⊢ ↑(↑n * π * 2) + ↑ψ = ↑ψ

Tactic:
mul_assoc,

Goal state after:
case mp.inr
θ ψ : ℝ
n : ℤ
hn : ↑n * π * 2 + ψ = θ
⊢ ↑(↑n * (π * 2)) + ↑ψ = ↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case inl.inr
n : ℤ
y : ℂ
hn : n ≠ 0
⊢ 0 ^ (↑n * y) = (0 ^ y) ^ n

Tactic:
rcases eq_or_ne y 0 with rfl | hy <;> simp [*, zero_zpow]

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

Goal state before:
pp: x : ℂ
n : ℤ
hlt : -π < x.arg * ↑n
hle : x.arg * ↑n ≤ π
y : ℂ
⊢ x ^ (↑n * y) = (x ^ n) ^ y

Tactic:
cpow_mul,

Goal state after:
x : ℂ
n : ℤ
hlt : -π < x.arg * ↑n
hle : x.arg * ↑n ≤ π
y : ℂ
⊢ (x ^ ↑n) ^ y = (x ^ n) ^ y

case h₁
x : ℂ
n : ℤ
hlt : -π < x.arg * ↑n
hle : x.arg * ↑n ≤ π
y : ℂ
⊢ -π < (log x * ↑n).im

case h₂
x : ℂ
n : ℤ
hlt : -π < x.arg * ↑n
hle : x.arg * ↑n ≤ π
y : ℂ
⊢ (log x * ↑n).im ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : ℝ
k : ℤ
H : θ + ψ = 2 * π * ↑k + π
⊢ θ + ψ = 2 * ↑k * π + π

Tactic:
mul_assoc,

Goal state after:
θ ψ : ℝ
k : ℤ
H : θ + ψ = 2 * (π * ↑k) + π
⊢ θ + ψ = 2 * ↑k * π + π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = ↑‖x‖ * ↑‖y‖ * (cexp (↑x.arg * I) * cexp (↑y.arg * I))

Tactic:
mul_assoc,

Goal state after:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = ↑‖x‖ * (↑‖y‖ * (cexp (↑x.arg * I) * cexp (↑y.arg * I)))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h.h
x✝¹ x✝ : ℝ
k : ℤ
h : 2 * (x✝¹ + x✝) = 2 * (2 * (2⁻¹ * π)) * ↑k + 2 * (2⁻¹ * π)
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹

Tactic:
mul_assoc,

Goal state after:
case h.h
x✝¹ x✝ : ℝ
k : ℤ
h : 2 * (x✝¹ + x✝) = 2 * (2 * (2⁻¹ * π) * ↑k) + 2 * (2⁻¹ * π)
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ.toReal ∈ Set.Ioo 0 π ↔ θ.sign = 1

Tactic:
rcases eq_or_ne θ π with rfl | h
  · simp
  · simp only [Set.mem_Ioo, ← sign_toReal h, sign_eq_one_iff, and_iff_left_iff_imp]
    exact fun _ ↦ (toReal_le_pi θ).lt_of_ne (toReal_eq_pi_iff.not.2 h)

Goal state after: