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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableConstSMul G α
s : Set α
hs : MeasurableSet s
a : G
⊢ MeasurableSet (a • s)

Tactic:
rw [← preimage_smul_inv]
  exact measurable_const_smul _ hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : SFinite μ
y : β
⊢ μ.prod (dirac y) = map (fun x ↦ (x, y)) μ

Tactic:
rw [← sum_sfiniteSeq μ, prod_sum_left, map_sum measurable_prodMk_right.aemeasurable]
  congr
  ext1 i
  refine prod_eq fun s t hs ht => ?_
  simp_rw [map_apply measurable_prodMk_right (hs.prod ht), mk_preimage_prod_left_eq_if, measure_if,
    dirac_apply' _ ht, ← indicator_mul_right _ fun _ => sfiniteSeq μ i s, Pi.one_apply, mul_one]

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

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
g : G
A : Set G
⊢ (Measure.map (fun h ↦ g * h) μ) A = μ A

Tactic:
map_mul_left_eq_self μ g

Goal state after:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
g : G
A : Set G
⊢ μ A = μ A
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
f : α × β → ℝ≥0∞
hf : AEMeasurable f (μ.prod ν)
⊢ AEMeasurable (fun x ↦ ∫⁻ (y : β), f (x, y) ∂ν) μ

Tactic:
by
  obtain ⟨g, hg, hfg⟩ := hf
  refine ⟨fun x ↦ ∫⁻ y, g (x, y) ∂ν, by fun_prop, ?_⟩
  exact (ae_ae_of_ae_prod hfg).mono fun x hfg' ↦ lintegral_congr_ae hfg'

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSpace H
inst✝¹ : Group G
μ : Measure G
inst✝ : MeasurableMul G
g : G
s : Set G
hs : MeasurableSet s
⊢ (map (fun x ↦ x * g) count) s = ↑s.encard

Tactic:
map_apply (measurable_mul_const _) hs,

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSpace H
inst✝¹ : Group G
μ : Measure G
inst✝ : MeasurableMul G
g : G
s : Set G
hs : MeasurableSet s
⊢ count ((fun x ↦ x * g) ⁻¹' s) = ↑s.encard
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s + ν s
h : μ s ≠ 0
h' : ν s = 0
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν) K

pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s + ν s
h : μ s ≠ 0
h' : ν s ≠ 0
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν) K

Tactic:
· simp only [h', add_zero] at hr
    rcases MeasurableSet.exists_lt_isCompact hs hr with ⟨K, Ks, hK, h'K⟩
    exact ⟨K, Ks, hK, h'K.trans_le (by simp)⟩

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s + ν s
h : μ s ≠ 0
h' : ν s ≠ 0
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν) K
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ μ ≪ map (fun x ↦ x * g) μ

Tactic:
refine AbsolutelyContinuous.mk fun s hs => ?_
  rw [map_apply (measurable_mul_const g) hs, measure_mul_right_null]; exact id

Goal state after:
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
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
⊢ ∀ᵐ (x : G) ∂μ', ν' ((fun y ↦ y * x) ⁻¹' s) < ∞

Tactic:
refine (ae_measure_preimage_mul_right_lt_top ν' ν' h3s).filter_mono ?_

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
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
⊢ ae μ' ≤ ae ν'
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a = f' a
h_a_nonneg : f' a ≠ 0
this : ↑(f' a) ≠ 0
⊢ ↑(f a) * g a = ↑(f' a) * g' a

Tactic:
rw [← h'a] at this ⊢

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a = f' a
h_a_nonneg : f' a ≠ 0
this : ↑(f a) ≠ 0
⊢ ↑(f a) * g a = ↑(f a) * g' a
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
x : α
hfx : ¬f x = ∞
⊢ ENNReal.ofReal (f x).toReal ≤ f x

Tactic:
· lift f x to ℝ≥0 using hfx with fx h
    simp

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

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

Tactic:
lintegral_withDensity_eq_lintegral_mul _ hf hg

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (f * g) a ∂μ = ∫⁻ (x : α) in s, (f * g) x ∂μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
M : MeasurableSet {x | f' x ≠ 0}ᶜ
x : α
hx : x ∈ {x | f' x ≠ 0}ᶜ
⊢ (f' * g') x = (f' * g) x

Tactic:
simp only [Classical.not_not, mem_ofPred_eq, mem_compl_iff] at hx

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
M : MeasurableSet {x | f' x ≠ 0}ᶜ
x : α
hx : f' x = 0
⊢ (f' * g') x = (f' * g) x
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: case mpr
x y : ℝ
h : 0 ≤ y
⊢ -√y ≤ x ∧ x ≤ √y → x ^ 2 ≤ y

Tactic:
rw [← abs_le, ← sq_abs]
    exact (le_sqrt (abs_nonneg x) h).mp

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

Goal state before:
pp: x : ℝ
⊢ 1 ≤ √x ↔ 1 ≤ x

Tactic:
rw [← sqrt_one, sqrt_le_sqrt_iff' zero_lt_one, sqrt_one]

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

Goal state before:
pp: n : ℤ
⊢ ‖↑n‖ = |↑n|

Tactic:
by
  rw [← ofReal_intCast, norm_real, Real.norm_eq_abs]

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

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
⊢ (cauSeqRe f).lim = f.lim.re

Tactic:
rw [lim_eq_lim_im_add_lim_re]; simp [ofReal]

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

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
⊢ (cauSeqIm f).lim = f.lim.im

Tactic:
rw [lim_eq_lim_im_add_lim_re]; simp [ofReal]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ (starRingEnd K) (r • z) = r • (starRingEnd K) z

Tactic:
by
  rw [conj_eq_re_sub_im, conj_eq_re_sub_im, smul_re, smul_im, ofReal_mul, ofReal_mul,
    real_smul_eq_coe_mul r (_ - _), mul_sub, mul_assoc]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
q : ℚ≥0
⊢ ‖↑↑q‖ = ↑q

Tactic:
exact norm_of_nonneg q.cast_nonneg

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
f : X → Y
h : IsOpenEmbedding f
inst✝ : Nonempty X
x : Y
hx : x ∈ range f
⊢ f (↑(toOpenPartialHomeomorph f h).symm x) = x

Tactic:
by
  rw [← congr_fun (h.toOpenPartialHomeomorph_apply f), OpenPartialHomeomorph.right_inv]
  rwa [toOpenPartialHomeomorph_target]

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
s : Set Z
x : Z
hx : f x ∈ e.source
h : f ⁻¹' e.source ∈ 𝓝[s] x
fe_cont : ContinuousWithinAt (↑e ∘ f) (s ∩ f ⁻¹' e.source) x
this : ContinuousWithinAt (↑e.symm ∘ ↑e ∘ f) (s ∩ f ⁻¹' e.source) x
⊢ f x = (↑e.symm ∘ ↑e ∘ f) x

Tactic:
by simp [e.left_inv hx]

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : TopologicalSpace α
x : α
s : Set α
C : ℝ
g : α → E
g' : α → F
h : ‖g x‖ ≤ C * ‖g' x‖
⊢ ((∀ᶠ (x : α) in pure x, ‖g x‖ ≤ C * ‖g' x‖) ∧ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖) ↔
    ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖

Tactic:
eventually_pure,

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : TopologicalSpace α
x : α
s : Set α
C : ℝ
g : α → E
g' : α → F
h : ‖g x‖ ≤ C * ‖g' x‖
⊢ (‖g x‖ ≤ C * ‖g' x‖ ∧ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖) ↔ ∀ᶠ (x : α) in 𝓝[s] x, ‖g x‖ ≤ C * ‖g' x‖
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case mpr
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
⊢ (∃ b, 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖) → (fun _x ↦ c) =O[l] f'

Tactic:
· rintro ⟨b, hb₀, hb⟩
    refine IsBigO.of_bound (‖c‖ / b) (hb.mono fun x hx => ?_)
    rw [div_mul_eq_mul_div, mul_div_assoc]
    exact le_mul_of_one_le_right (norm_nonneg _) ((one_le_div hb₀).2 hx)

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
⊢ (fun _x ↦ c) =O[l] f' ↔ ∃ b, 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖

Tactic:
constructor
  · intro h
    rcases h.exists_pos with ⟨C, hC₀, hC⟩
    refine ⟨‖c‖ / C, div_pos (norm_pos_iff.2 hc) hC₀, ?_⟩
    exact hC.bound.mono fun x => (div_le_iff₀' hC₀).2
  · rintro ⟨b, hb₀, hb⟩
    refine IsBigO.of_bound (‖c‖ / b) (hb.mono fun x hx => ?_)
    rw [div_mul_eq_mul_div, mul_div_assoc]
    exact le_mul_of_one_le_right (norm_nonneg _) ((one_le_div hb₀).2 hx)

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

Goal state before:
pp: x : ℝ
⊢ (starRingEnd ℂ) (cexp ↑x) = cexp ↑x

Tactic:
← exp_conj,

Goal state after:
x : ℝ
⊢ cexp ((starRingEnd ℂ) ↑x) = cexp ↑x
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
n : ℤ
hn : Odd n
⊢ a ^ n ≤ 0 ↔ a ≤ 0

Tactic:
rw [le_iff_lt_or_eq, le_iff_lt_or_eq, hn.zpow_neg_iff, zpow_eq_zero_iff]
  rintro rfl
  exact Int.not_even_iff_odd.2 hn .zero

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

Goal state before:
pp: x : ℝ
n : ℕ
⊢ sin (↑n * π - x) = -((-1) ^ n * sin x)

Tactic:
simpa only [sin_neg, mul_neg] using sin_antiperiodic.nat_mul_sub_eq n

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

Goal state before:
pp: c : ℝ
hc : c < 0
f : ℕ → ℝ
hf : ∀ (i : ℕ), ↑i ≤ f i
i : ℕ
⊢ c * f i ≤ ↑i * c

Tactic:
conv_rhs => rw [mul_comm]

Goal state after:
c : ℝ
hc : c < 0
f : ℕ → ℝ
hf : ∀ (i : ℕ), ↑i ≤ f i
i : ℕ
⊢ c * f i ≤ c * ↑i
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
⊢ cos x = 0 ↔ sin x * sin x = sin ?m.18 * sin ?m.18 + cos ?m.18 * cos ?m.18

pp: x : ℝ
⊢ ℝ

Tactic:
left_eq_add,

Goal state after:
x : ℝ
⊢ cos x = 0 ↔ cos x * cos x = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y - x) / 2)
⊢ 0 < 2 * sin ((y - x) / 2) * cos ((y + x) / 2)

Tactic:
have : 0 < cos ((y + x) / 2) := by refine cos_pos_of_mem_Ioo ⟨?_, ?_⟩ <;> linarith

Goal state after:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this✝ : 0 < sin ((y - x) / 2)
this : 0 < cos ((y + x) / 2)
⊢ 0 < 2 * sin ((y - x) / 2) * cos ((y + x) / 2)
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ closedBall x δ * s = x • cthickening δ s

Tactic:
rw [mul_comm, hs.mul_closedBall hδ]

Goal state after:
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✝ : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < ‖(mk I) a‖ + ε₁
b : R
hb : ‖b‖ < ‖(mk I) b‖ + ε₂
h :
  ∀ (a_1 b_1 : ℝ),
    a_1 - ‖(mk I) a‖ < ε₁ ∧ ‖(mk I) a‖ - a_1 < ε₁ →
      b_1 - ‖(mk I) b‖ < ε₂ ∧ ‖(mk I) b‖ - b_1 < ε₂ →
        a_1 * b_1 - ‖(mk I) a‖ * ‖(mk I) b‖ < ε ∧ ‖(mk I) a‖ * ‖(mk I) b‖ - a_1 * b_1 < ε
⊢ ‖(mk I) a‖ - ‖a‖ < ε₁

Tactic:
linarith [Ideal.Quotient.norm_mk_le I a]

Goal state after:
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✝ : SeminormedCommRing R
I : Ideal R
x y : R ⧸ I
ε : ℝ
hε : 0 < ε
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖ + ε

Tactic:
by
    have := ((nhds_basis_ball.prod_nhds nhds_basis_ball).tendsto_iff nhds_basis_ball).mp
      (continuous_mul.tendsto (‖x‖, ‖y‖)) ε hε
    simp only [Set.mem_prod, mem_ball, and_imp, Prod.forall, Prod.exists] at this
    rcases this with ⟨ε₁, ε₂, ⟨h₁, h₂⟩, h⟩
    obtain ⟨⟨a, rfl, ha⟩, ⟨b, rfl, hb⟩⟩ := Ideal.Quotient.norm_mk_lt x h₁,
      Ideal.Quotient.norm_mk_lt y h₂
    simp only [dist, abs_sub_lt_iff] at h
    specialize h ‖a‖ ‖b‖ ⟨by linarith, by linarith [Ideal.Quotient.norm_mk_le I a]⟩
      ⟨by linarith, by linarith [Ideal.Quotient.norm_mk_le I b]⟩
    calc
      _ ≤ ‖a‖ * ‖b‖ := (Ideal.Quotient.norm_mk_le I (a * b)).trans (norm_mul_le a b)
      _ ≤ _ := (sub_lt_iff_lt_add'.mp h.1).le

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ closedBall x r \ interior (closedBall x r) = sphere x r

Tactic:
interior_closedBall x hr,

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ closedBall x r \ ball x r = sphere x r
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 3) ^ 2 = 3 / 4

Tactic:
rw [← cos_pi_div_two_sub, ← sq_cos_pi_div_six]
  congr
  ring

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

Goal state before:
pp: z : ℂ
⊢ cos z = 0 ↔ sin z * sin z = sin ?m.18 * sin ?m.18 + cos ?m.18 * cos ?m.18

pp: z : ℂ
⊢ ℂ

Tactic:
left_eq_add,

Goal state after:
z : ℂ
⊢ cos z = 0 ↔ cos z * cos z = 0
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
⊢ ‖↑x‖ = |x|

Tactic:
suffices round (p⁻¹ * x) = 0 by simp [norm_eq, this]

Goal state after:
case inr
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
⊢ round (p⁻¹ * x) = 0
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inl
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : |p| / 2 ≤ ε
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < |p| / 2 then closedBall x ε ∩ s else s

Tactic:
rcases eq_or_ne p 0 with (rfl | hp)
    · simp only [abs_zero, zero_div] at hε
      simp only [not_lt.mpr hε, coe_real_preimage_closedBall_period_zero, abs_zero, zero_div,
        if_false, inter_eq_right]
      exact hs.trans (closedBall_subset_closedBall <| by simp [hε])
    simp [closedBall_eq_univ_of_half_period_le p hp (↑x) hε, not_lt.mpr hε]

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

Goal state before:
pp: case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ cos (arcsin x) = √(1 - x ^ 2)

Tactic:
rw [not_le] at hx₂
    rw [arcsin_of_one_le hx₂.le, cos_pi_div_two, sqrt_eq_zero_of_nonpos]
    nlinarith

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

Goal state before:
pp: case refine_1
z : ℂ
hz : ‖z‖ = 1
⊢ cexp (↑z.arg * I) = z

pp: case refine_2
z : ℂ
⊢ (∃ θ, cexp (↑θ * I) = z) → ‖z‖ = 1

Tactic:
· calc
      exp (arg z * I) = ‖z‖ * exp (arg z * I) := by rw [hz, ofReal_one, one_mul]
      _ = z := norm_mul_exp_arg_mul_I z

Goal state after:
case refine_2
z : ℂ
⊢ (∃ θ, cexp (↑θ * I) = z) → ‖z‖ = 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case neg
x : ℝ
hx0 : ¬x ≤ 0
h : rexp (log x) * rexp 1 ≤ rexp (rexp (log x))
⊢ rexp 1 * x ≤ rexp x

Tactic:
exp_log (lt_of_not_ge hx0),

Goal state after:
case neg
x : ℝ
hx0 : ¬x ≤ 0
h : x * rexp 1 ≤ rexp x
⊢ rexp 1 * x ≤ rexp x
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f₁ f₂ : α → K
g : α → R
t : R
l : Filter α
hmul : Tendsto (fun x ↦ f₁ x • g x) l (𝓝 t)
hf₁ : Tendsto f₁ l (cobounded K)
hbdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f₁ x - f₂ x‖
⊢ Tendsto (fun x ↦ ‖f₁ x • g x - f₂ x • g x‖) l (𝓝 0)

Tactic:
← sub_smul,

Goal state after:
α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f₁ f₂ : α → K
g : α → R
t : R
l : Filter α
hmul : Tendsto (fun x ↦ f₁ x • g x) l (𝓝 t)
hf₁ : Tendsto f₁ l (cobounded K)
hbdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f₁ x - f₂ x‖
⊢ Tendsto (fun x ↦ ‖(f₁ x - f₂ x) • g x‖) l (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x.arg = y.arg ↔ ↑‖y‖ / ↑‖x‖ * x = y

Tactic:
simp only [ext_norm_arg_iff, norm_mul, norm_div, norm_real, norm_norm,
    div_mul_cancel₀ _ (norm_ne_zero_iff.mpr hx), true_and]

Goal state after:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x.arg = y.arg ↔ (↑‖y‖ / ↑‖x‖ * x).arg = y.arg
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case hg
α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f₁ f₂ : α → K
g : α → R
t : R
l : Filter α
hmul : Tendsto (fun x ↦ f₁ x • g x) l (𝓝 t)
hf₁ : Tendsto f₁ l (cobounded K)
hbdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f₁ x - f₂ x‖
⊢ Tendsto g l (𝓝 0)

Tactic:
exact tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded hmul.norm.isBoundedUnder_le hf₁

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

Goal state before:
pp: x : ℂ
⊢ (log x).re = Real.log ‖x‖

Tactic:
by simp [log]

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

Goal state before:
pp: x : ℂ
⊢ (log x).im = x.arg

Tactic:
by simp [log]

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

Goal state before:
pp: ⊢ log 0 = 0

Tactic:
by simp [log]

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

Goal state before:
pp: ⊢ log 1 = 0

Tactic:
by simp [log]

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

Goal state before:
pp: x : ℂ
⊢ log (x / x) = 0

Tactic:
by simp [log]

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

Goal state before:
pp: ⊢ log (-1) = ↑π * I

Tactic:
by simp [log]

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

Goal state before:
pp: ⊢ log I = ↑π / 2 * I

Tactic:
by simp [log]

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

Goal state before:
pp: ⊢ log (-I) = -(↑π / 2) * I

Tactic:
by simp [log]

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

Goal state before:
pp: x : ℝ
n : ℕ
⊢ ↑(↑n * x) = n • ↑x

Tactic:
simpa only [nsmul_eq_mul] using! coeHom.map_nsmul n x

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

Goal state before:
pp: case refine_1
s : Set ℂ
hs : (cexp ⁻¹' s).Countable
⊢ s ⊆ insert 0 (s \ {0})

Tactic:
← Set.union_singleton,

Goal state after:
case refine_1
s : Set ℂ
hs : (cexp ⁻¹' s).Countable
⊢ s ⊆ s \ {0} ∪ {0}
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x y : ℂ
⊢ x ^ (-y) = (x ^ y)⁻¹

Tactic:
simp only [cpow_def, neg_eq_zero, mul_neg]
  split_ifs <;> simp [exp_neg]

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

Goal state before:
pp: x n : ℂ
⊢ (if x⁻¹ = 0 then if n = 0 then 1 else 0 else cexp ((if x.arg = π then -(starRingEnd ℂ) (log x) else -log x) * n)) =
    if x.arg = π then
      (starRingEnd ℂ) (if x = 0 then if (starRingEnd ℂ) n = 0 then 1 else 0 else cexp (log x * (starRingEnd ℂ) n))⁻¹
    else (if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n))⁻¹

Tactic:
inv_eq_zero,

Goal state after:
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0 else cexp ((if x.arg = π then -(starRingEnd ℂ) (log x) else -log x) * n)) =
    if x.arg = π then
      (starRingEnd ℂ) (if x = 0 then if (starRingEnd ℂ) n = 0 then 1 else 0 else cexp (log x * (starRingEnd ℂ) n))⁻¹
    else (if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ -(π / 2) < z.arg ∧ (0 < z.re ∨ z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0

Tactic:
neg_pi_div_two_lt_arg_iff,

Goal state after:
z : ℂ
⊢ (0 < z.re ∨ 0 ≤ z.im) ∧ (0 < z.re ∨ z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0
    else if x.arg = π then (cexp ((starRingEnd ℂ) (log x) * n))⁻¹ else (cexp (log x * n))⁻¹) =
    if x.arg = π then if x = 0 then if n = 0 then 1 else 0 else ((starRingEnd ℂ) (cexp (log x * (starRingEnd ℂ) n)))⁻¹
    else if x = 0 then if n = 0 then 1 else 0 else (cexp (log x * n))⁻¹

Tactic:
← exp_conj,

Goal state after:
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0
    else if x.arg = π then (cexp ((starRingEnd ℂ) (log x) * n))⁻¹ else (cexp (log x * n))⁻¹) =
    if x.arg = π then if x = 0 then if n = 0 then 1 else 0 else (cexp ((starRingEnd ℂ) (log x * (starRingEnd ℂ) n)))⁻¹
    else if x = 0 then if n = 0 then 1 else 0 else (cexp (log x * n))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ.cos = 0 ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)

Tactic:
rw [← cos_pi_div_two, ← cos_coe, cos_eq_iff_eq_or_eq_neg, ← coe_neg, ← neg_div]

Goal state after: