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

Goal state before:
pp: case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
n : ℕ
⊢ (μ.withDensity fun x ↦ ↑(f x)) (spanningSets μ n ∩ f ⁻¹' Iic ↑n) < ∞

Tactic:
withDensity_apply'

Goal state after:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f : α → ℝ≥0
n : ℕ
⊢ ∫⁻ (a : α) in spanningSets μ n ∩ f ⁻¹' Iic ↑n, ↑(f a) ∂μ < ∞
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ ∀ (a b c : ℂ), a * (b + c) = a * b + a * c

Tactic:
intros; ext <;> simp [mul_re, mul_im] <;> ring

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

Goal state before:
pp: ⊢ ∀ (a b c : ℂ), (a + b) * c = a * c + b * c

Tactic:
intros; ext <;> simp [mul_re, mul_im] <;> ring

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x | f x = ∞}
hs : MeasurableSet s
key : μ.withDensity f = μ.withDensity (sᶜ.indicator f) + sum fun x ↦ μ.withDensity (s.indicator 1)
this : SigmaFinite (μ.withDensity (sᶜ.indicator f))
⊢ SigmaFinite (μ.withDensity (s.indicator 1))

Tactic:
withDensity_indicator hs

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x | f x = ∞}
hs : MeasurableSet s
key : μ.withDensity f = μ.withDensity (sᶜ.indicator f) + sum fun x ↦ μ.withDensity (s.indicator 1)
this : SigmaFinite (μ.withDensity (sᶜ.indicator f))
⊢ SigmaFinite ((μ.restrict s).withDensity 1)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: z : ℂ
h : z ≠ 0
⊢ z * z⁻¹ = 1

Tactic:
inv_def,

Goal state after:
z : ℂ
h : z ≠ 0
⊢ z * ((starRingEnd ℂ) z * ↑(normSq z)⁻¹) = 1
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : ExistsAddOfLE R
inst✝¹ : Module ℚ≥0 R
inst✝ : PosSMulMono ℚ≥0 R
s : Finset ι
f g : ι → R
⊢ (𝔼 i ∈ s, f i * g i) ^ 2 ≤ (𝔼 i ∈ s, f i ^ 2) * 𝔼 i ∈ s, g i ^ 2

Tactic:
simp only [expect, smul_pow, inv_pow, smul_mul_smul_comm, ← sq]

Goal state after:
ι : Type u_1
R : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : ExistsAddOfLE R
inst✝¹ : Module ℚ≥0 R
inst✝ : PosSMulMono ℚ≥0 R
s : Finset ι
f g : ι → R
⊢ (↑(#s) ^ 2)⁻¹ • (∑ x ∈ s, f x * g x) ^ 2 ≤ (↑(#s) ^ 2)⁻¹ • ((∑ x ∈ s, f x ^ 2) * ∑ x ∈ s, g x ^ 2)
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ μ.withDensity f ∗ₘ μ.withDensity g = μ.withDensity (f ⋆ₘₗ[μ] g)

Tactic:
refine ext_of_lintegral _ fun φ hφ ↦ ?_
  rw [lintegral_mconv_eq_lintegral_prod hφ, prod_withDensity₀ hf hg,
    lintegral_withDensity_eq_lintegral_mul₀,
    lintegral_withDensity_eq_lintegral_mul₀, lintegral_prod,
    lintegral_congr (fun x ↦ by apply (lintegral_mul_left_eq_self _ x⁻¹).symm),
    lintegral_lintegral_swap]
  · simp only [Pi.mul_apply, mul_inv_cancel_left, mlconvolution_def]
    conv in (∫⁻ _, _ ∂μ) * φ _ => rw [(lintegral_mul_const'' _ (by fun_prop)).symm]
  all_goals first | fun_prop | dsimp; fun_prop

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
u : R
hu : IsUnit u
h_mul : star u * u = 1
⊢ u * star u = 1

Tactic:
lift u to Rˣ using hu

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
u : Rˣ
h_mul : star ↑u * ↑u = 1
⊢ ↑u * star ↑u = 1
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CStarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CStarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CStarRing (R i)
x : (i : ι) → R i
⊢ ‖x‖ * ‖x‖ ≤ ‖x⋆ * x‖

Tactic:
refine le_of_eq (Eq.symm ?_)

Goal state after:
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CStarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CStarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CStarRing (R i)
x : (i : ι) → R i
⊢ ‖x⋆ * x‖ = ‖x‖ * ‖x‖
Module: Mathlib.Analysis.Complex.Basic

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

Tactic:
ext1 z
  dsimp
  apply mul_comm

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ re z⁻¹ = re z / normSq z

Tactic:
inv_def,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ re ((starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹) = re z / normSq z
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ im z⁻¹ = -im z / normSq z

Tactic:
inv_def,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ im ((starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹) = -im z / normSq z
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
x : A
⊢ Commute (star x) x ↔ Commute ↑(ℜ x) ↑(ℑ x)

Tactic:
commute_iff_eq,

Goal state after:
A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
x : A
⊢ star x * x = x * star x ↔ Commute ↑(ℜ x) ↑(ℑ x)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
a : K
h : ‖a‖ ≤ re a
⊢ im a = 0

Tactic:
im_eq_zero_of_le h

Goal state after:
K : Type u_1
inst✝ : RCLike K
a : K
h : ‖a‖ ≤ re a
⊢ 0 = 0
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: x : ℝ
⊢ normSq x = x * x

Tactic:
simp [RCLike.normSq]

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
f : α → E
g : α → F
l : Filter α
⊢ f =O[l] g ↔ ∃ c, IsBigOWith c l f g

Tactic:
IsBigO_def

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
⊢ (∃ c, IsBigOWith c l f g) ↔ ∃ c, IsBigOWith c l f g
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
c : ℝ
f : α → E
g : α → F
l : Filter α
h : IsBigOWith c l f g
⊢ f =O[l] g

Tactic:
IsBigO_def

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
l : Filter α
h : IsBigOWith c l f g
⊢ ∃ c, IsBigOWith c l f g
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ
hf : 1 ≤ᶠ[l] f
m n : ℕ
h : n ≤ m
⊢ (f ^ n) =O[l] (f ^ m)

Tactic:
IsBigO_def

Goal state after:
α : Type u_1
l : Filter α
f : α → ℝ
hf : 1 ≤ᶠ[l] f
m n : ℕ
h : n ≤ m
⊢ ∃ c, IsBigOWith c l (f ^ n) (f ^ m)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cosh x ^ 2 = sinh x ^ 2 + 1

Tactic:
by
  rw [← cosh_sq_sub_sinh_sq x]
  ring

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

Goal state before:
pp: x : ℂ
⊢ sinh x ^ 2 = cosh x ^ 2 - 1

Tactic:
by
  rw [← cosh_sq_sub_sinh_sq x]
  ring

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

Goal state before:
pp: case h₂
α : 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
hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε
hNMK : max N M + 1 < K
hKN : N < K
m : ℕ
hmJ : m ∈ range (max N M + 1)
⊢ N ≤ max N M + 1

Tactic:
exact Nat.le_succ_of_le (le_max_left _ _)

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

Goal state before:
pp: n : ℕ
z : ℂ
⊢ (cos z + sin z * I) ^ n = cos (↑n * z) + sin (↑n * z) * I

Tactic:
← exp_mul_I,

Goal state after:
n : ℕ
z : ℂ
⊢ cexp (z * I) ^ n = cos (↑n * z) + sin (↑n * z) * I
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: n : ℕ
z : ℂ
⊢ cexp (z * I) ^ n = cos (↑n * z) + sin (↑n * z) * I

Tactic:
← exp_mul_I,

Goal state after:
n : ℕ
z : ℂ
⊢ cexp (z * I) ^ n = cexp (↑n * z * I)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
F' : Type u_7
inst✝² : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst✝¹ : Fintype ι
E' : ι → Type u_18
inst✝ : (i : ι) → SeminormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
⊢ f =O[l] g' ↔ ∀ (i : ι), (fun x ↦ f x i) =O[l] g'

Tactic:
simp only [isBigO_iff_eventually_isBigOWith, ← eventually_all]

Goal state after:
α : Type u_1
F' : Type u_7
inst✝² : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst✝¹ : Fintype ι
E' : ι → Type u_18
inst✝ : (i : ι) → SeminormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
⊢ (∀ᶠ (c : ℝ) in atTop, IsBigOWith c l f g') ↔ ∀ᶠ (x : ℝ) in atTop, ∀ (i : ι), IsBigOWith x l (fun x ↦ f x i) g'
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: n : ℕ
x r₁ r₂ : ℝ
⊢ expNear n x r₁ - expNear n x r₂ = x ^ n / ↑n.factorial * (r₁ - r₂)

Tactic:
simp [expNear, mul_sub]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.ModEq

Goal state before:
pp: ⊢ ∃ᶠ (m : ℕ) in atTop, Even m

Tactic:
simpa only [even_iff] using frequently_mod_eq zero_lt_two

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

Goal state before:
pp: case pos
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h✝ : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 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‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun n ↦ ‖f n‖ / ‖g n‖
C₁_mem : C₁ ∈ ubounds
n : ℕ
h_ind : ∀ m < n, n₁ ≤ m → ‖f m‖ ≤ max C₀ C₁ * ‖g m‖
hn : n₁ ≤ n
m : ℕ
hm : m ∈ Finset.Ico n₀ n
hbase : m < n₁
⊢ ‖f m‖ ≤ max C₀ C₁ * ‖g m‖

Tactic:
have hC₁ : C₁ ≤ max C₀ C₁ := by grind

Goal state after:
case pos
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h✝ : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 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‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun n ↦ ‖f n‖ / ‖g n‖
C₁_mem : C₁ ∈ ubounds
n : ℕ
h_ind : ∀ m < n, n₁ ≤ m → ‖f m‖ ≤ max C₀ C₁ * ‖g m‖
hn : n₁ ≤ n
m : ℕ
hm : m ∈ Finset.Ico n₀ n
hbase : m < n₁
hC₁ : C₁ ≤ max C₀ C₁
⊢ ‖f m‖ ≤ max C₀ C₁ * ‖g m‖
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: case hx
x : ℝ
⊢ 0 ≤ rexp x

Tactic:
exact (exp_pos _).le

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

Goal state before:
pp: case hy
x : ℝ
⊢ 0 ≤ rexp (x / 2)

Tactic:
exact (exp_pos _).le

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

Goal state before:
pp: case inl
x : ℝ
hx : |x| ≤ π
h : x < 0
⊢ |sin x| = -sin x

Tactic:
abs_of_nonpos (sin_nonpos_of_nonpos_of_neg_pi_le h.le (abs_le.1 hx).1)

Goal state after:
case inl
x : ℝ
hx : |x| ≤ π
h : x < 0
⊢ -sin x = -sin x
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 : ℝ
⊢ ∀ (a : M), a ∈ {m | ↑m = x⁻¹} → r ≤ dist 1 a ↔ (Equiv.inv M) a ∈ {m | ↑m = x} → r ≤ dist 1 ((Equiv.inv M) a)

Tactic:
by simp [← inv_eq_iff_eq_inv]

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
this : ∀ (ε : ℝ), mk '' ball 1 ε = {x | ‖x‖ < ε}
⊢ (𝓝 ↑1).HasBasis (fun ε ↦ 0 < ε) fun ε ↦ {x | ‖x‖ < ε}

Tactic:
nhds_eq,

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
this : ∀ (ε : ℝ), mk '' ball 1 ε = {x | ‖x‖ < ε}
⊢ (Filter.map mk (𝓝 1)).HasBasis (fun ε ↦ 0 < ε) fun ε ↦ {x | ‖x‖ < ε}
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case hx
n : ℕ
⊢ 0 ≤ 2 - sqrtTwoAddSeries 0 n

Tactic:
sub_nonneg

Goal state after:
case hx
n : ℕ
⊢ sqrtTwoAddSeries 0 n ≤ 2
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ interior (sphere x r) = ∅

Tactic:
rw [← frontier_closedBall' x, interior_frontier isClosed_closedBall]

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

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

Tactic:
trans sin (π / 2 ^ 2)

Goal state after:
⊢ sin (π / 4) = sin (π / 2 ^ 2)

⊢ sin (π / 2 ^ 2) = √2 / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: c : ℝ := cos (π / 5)
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 ∈ Icc (-(π / 2)) (π / 2)

Tactic:
constructor <;> linarith [pi_pos.le]

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

Goal state before:
pp: K : Type u_4
inst✝ : NormedDivisionRing K
ξ : K
h : Summable fun n ↦ ξ ^ n
⊢ ‖ξ‖ < 1

Tactic:
obtain ⟨k : ℕ, hk : dist (ξ ^ k) 0 < 1⟩ :=
    (h.tendsto_cofinite_zero.eventually (ball_mem_nhds _ zero_lt_one)).exists

Goal state after:
K : Type u_4
inst✝ : NormedDivisionRing K
ξ : K
h : Summable fun n ↦ ξ ^ n
k : ℕ
hk : dist (ξ ^ k) 0 < 1
⊢ ‖ξ‖ < 1
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
γ : Path (p 0) (p (last n))
h₁ : ∀ (y : ↑I), γ y ∈ s
h₂ : ∀ (i : Fin (n + 1)), ∃ y, γ y = p i
⊢ ∃ γ t, (∀ (t : ↑I), γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), γ (t i) = p i

Tactic:
choose! t ht using h₂

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
γ : Path (p 0) (p (last n))
h₁ : ∀ (y : ↑I), γ y ∈ s
t : Fin (n + 1) → ↑I
ht : ∀ (i : Fin (n + 1)), γ (t i) = p i
⊢ ∃ γ t, (∀ (t : ↑I), γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), γ (t i) = p i
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
T : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace T
t : Set X
f : T → X → Y
g : C(↑t, Y)
f_cont : ContinuousOn (Function.uncurry f) (univ ×ˢ t)
this : ∀ (x : T), ContinuousOn (f x) t
⊢ Continuous[instTopologicalSpaceProd, inst✝¹]
    (Function.uncurry fun x y ↦ { toFun := t.domRestrict (f x), continuous_toFun := ⋯ } y)

Tactic:
exact f_cont.comp_continuous (.prodMap continuous_id continuous_subtype_val)
    fun xz ↦ ⟨trivial, xz.2.2⟩

Goal state after:
Module: Mathlib.Topology.Instances.Sign

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

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

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✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : ¬t₀ ≤ ↑1
h₃ : t₀ ≤ t₁
⊢ 1 < t₀

Tactic:
simpa using h₁

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

Goal state before:
pp: x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
⊢ sin (arcsin (sin x)) = sin x

Tactic:
sin_arcsin (neg_one_le_sin _) (sin_le_one _)

Goal state after:
x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
⊢ sin x = sin x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
⊢ ↑‖x‖ * (cos ↑x.arg + sin ↑x.arg * I) = x

Tactic:
← exp_mul_I,

Goal state after:
x : ℂ
⊢ ↑‖x‖ * cexp (↑x.arg * I) = x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
hx : x ≤ -1
⊢ arccos x = π

Tactic:
rw [arccos, arcsin_of_le_neg_one hx, sub_neg_eq_add, add_halves]

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

Goal state before:
pp: x : ℝ
hx : x ≤ -1
⊢ arccos x = π

Tactic:
by
  rw [arccos, arcsin_of_le_neg_one hx, sub_neg_eq_add, add_halves]

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

Goal state before:
pp: θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ (cos ↑θ + sin ↑θ * I).arg = θ

Tactic:
by
  rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I zero_lt_one hθ]

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

Goal state before:
pp: z : ℂ
⊢ (cexp z).arg =
    (↑(rexp z.re) * (cos ↑(toIocMod Real.two_pi_pos (-π) z.im) + sin ↑(toIocMod Real.two_pi_pos (-π) z.im) * I)).arg

Tactic:
← exp_mul_I,

Goal state after:
z : ℂ
⊢ (cexp z).arg = (↑(rexp z.re) * cexp (↑(toIocMod Real.two_pi_pos (-π) z.im) * I)).arg
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: ⊢ StrictAntiOn log (Iio 0)

Tactic:
rintro x (hx : x < 0) y (hy : y < 0) hxy
  rw [← log_abs y, ← log_abs x]
  refine log_lt_log (abs_pos.2 hy.ne) ?_
  rwa [abs_of_neg hy, abs_of_neg hx, neg_lt_neg_iff]

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ log (√x ^ 2) = log x

pp: x : ℝ
hx : 0 ≤ x
⊢ 2 ≠ 0

Tactic:
sq_sqrt hx

Goal state after:
x : ℝ
hx : 0 ≤ x
⊢ log x = log x

x : ℝ
hx : 0 ≤ x
⊢ 2 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π

Tactic:
rcases lt_trichotomy x.re 0 with (hr | hr | hr)

Goal state after:
case inl
x : ℂ
hr : x.re < 0
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π

case inr.inl
x : ℂ
hr : x.re = 0
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π

case inr.inr
x : ℂ
hr : 0 < x.re
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case neg
x : ℂ
hx : ¬x = 0
⊢ log x⁻¹ = if x.arg = π then -(starRingEnd ℂ) (log x) else -log x

Tactic:
inv_def,

Goal state after:
case neg
x : ℂ
hx : ¬x = 0
⊢ log ((starRingEnd ℂ) x * ↑(normSq x)⁻¹) = if x.arg = π then -(starRingEnd ℂ) (log x) else -log x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
⊢ x⁻¹.arg = ((starRingEnd ℂ) x).arg

Tactic:
inv_def,

Goal state after:
x : ℂ
⊢ ((starRingEnd ℂ) x * ↑(normSq x)⁻¹).arg = ((starRingEnd ℂ) x).arg
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
by
  rw [← arg_conj, inv_def, mul_comm]
  by_cases hx : x = 0
  · simp [hx]
  · exact arg_real_mul (conj x) (by simp [hx])

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

Goal state before:
pp: case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ Real.arcsin ((-z).im / ‖z‖) < π + -(π / 2)

Tactic:
←
      sub_eq_add_neg,

Goal state after:
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ Real.arcsin ((-z).im / ‖z‖) < π - π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
← cos_coe,

Goal state after:
θ : Angle
⊢ θ.cos = (↑(π / 2)).cos ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl
x : ℂ
hi : x.im = 0
⊢ (-↑x.re).arg = (↑x.re).arg - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0

Tactic:
rcases lt_trichotomy x.re 0 with (hr | hr | hr)

Goal state after:
case inr.inl.inl
x : ℂ
hi : x.im = 0
hr : x.re < 0
⊢ (-↑x.re).arg = (↑x.re).arg - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0

case inr.inl.inr.inl
x : ℂ
hi : x.im = 0
hr : x.re = 0
⊢ (-↑x.re).arg = (↑x.re).arg - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0

case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ (-↑x.re).arg = (↑x.re).arg - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl
x : ℂ
hi : x.im = 0
⊢ (-↑x.re).arg = (↑x.re).arg + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re

Tactic:
rcases lt_trichotomy x.re 0 with (hr | hr | hr)

Goal state after:
case inr.inl.inl
x : ℂ
hi : x.im = 0
hr : x.re < 0
⊢ (-↑x.re).arg = (↑x.re).arg + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re

case inr.inl.inr.inl
x : ℂ
hi : x.im = 0
hr : x.re = 0
⊢ (-↑x.re).arg = (↑x.re).arg + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re

case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ (-↑x.re).arg = (↑x.re).arg + π ↔ (↑x.re).im < 0 ∨ (↑x.re).im = 0 ∧ 0 < (↑x.re).re