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
μ : Measure G
inst✝² : SFinite μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
y : G
⊢ μ ((fun x ↦ x * y) ⁻¹' s) = 0 ↔ μ ((fun x ↦ (y⁻¹ * x⁻¹)⁻¹) ⁻¹' s) = 0

Tactic:
mul_inv_rev,

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
y : G
⊢ μ ((fun x ↦ x * y) ⁻¹' s) = 0 ↔ μ ((fun x ↦ x⁻¹⁻¹ * y⁻¹⁻¹) ⁻¹' s) = 0
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✝ : μ.IsMulRightInvariant
g : G
this✝ : QuasiMeasurePreserving (fun h ↦ h * g⁻¹) μ μ
this : QuasiMeasurePreserving (fun x ↦ (x⁻¹ * g⁻¹)⁻¹) μ μ
⊢ QuasiMeasurePreserving (fun h ↦ g * h) μ μ

Tactic:
mul_inv_rev,

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
g : G
this✝ : QuasiMeasurePreserving (fun h ↦ h * g⁻¹) μ μ
this : QuasiMeasurePreserving (fun x ↦ g⁻¹⁻¹ * x⁻¹⁻¹) μ μ
⊢ QuasiMeasurePreserving (fun h ↦ g * h) μ μ
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b c x : R
h : a * (x * x) + b * x + c = 0
⊢ discrim a b c = (2 * a * x + b) ^ 2

Tactic:
rw [discrim]

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b c x : R
h : a * (x * x) + b * x + c = 0
⊢ b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ HasFiniteIntegral (fun x ↦ (f x).toReal) μ

Tactic:
by
  have h x : ‖(f x).toReal‖ₑ = .ofReal (f x).toReal := by
    rw [Real.enorm_of_nonneg ENNReal.toReal_nonneg]
  simp_rw [hasFiniteIntegral_iff_enorm, h]
  refine lt_of_le_of_lt (lintegral_mono fun x => ?_) (lt_top_iff_ne_top.2 hf)
  by_cases hfx : f x = ∞
  · simp [hfx]
  · lift f x to ℝ≥0 using hfx with fx h
    simp

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

Goal state before:
pp: x : ℝ≥0
⊢ ↑(NNReal.sqrt x) = √↑x

Tactic:
Real.sqrt,

Goal state after:
x : ℝ≥0
⊢ ↑(NNReal.sqrt x) = ↑(NNReal.sqrt (↑x).toNNReal)
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
h : 0 ≤ x
⊢ √x * √x = x

Tactic:
Real.sqrt,

Goal state after:
x : ℝ
h : 0 ≤ x
⊢ ↑(NNReal.sqrt x.toNNReal) * ↑(NNReal.sqrt x.toNNReal) = x
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ √x ≤ √y ↔ x ≤ y

Tactic:
Real.sqrt,

Goal state after:
x y : ℝ
hy : 0 ≤ y
⊢ ↑(NNReal.sqrt x.toNNReal) ≤ √y ↔ x ≤ y
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ ↑(NNReal.sqrt x.toNNReal) ≤ √y ↔ x ≤ y

Tactic:
Real.sqrt,

Goal state after:
x y : ℝ
hy : 0 ≤ y
⊢ ↑(NNReal.sqrt x.toNNReal) ≤ ↑(NNReal.sqrt y.toNNReal) ↔ x ≤ y
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hy : 0 < y
⊢ √x < √y ↔ x < y

Tactic:
Real.sqrt,

Goal state after:
x y : ℝ
hy : 0 < y
⊢ ↑(NNReal.sqrt x.toNNReal) < √y ↔ x < y
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hy : 0 < y
⊢ ↑(NNReal.sqrt x.toNNReal) < √y ↔ x < y

Tactic:
Real.sqrt,

Goal state after:
x y : ℝ
hy : 0 < y
⊢ ↑(NNReal.sqrt x.toNNReal) < ↑(NNReal.sqrt y.toNNReal) ↔ x < y
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
h : x ≤ y
⊢ √x ≤ √y

Tactic:
Real.sqrt,

Goal state after:
x y : ℝ
h : x ≤ y
⊢ ↑(NNReal.sqrt x.toNNReal) ≤ √y
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
h : x ≤ y
⊢ ↑(NNReal.sqrt x.toNNReal) ≤ √y

Tactic:
Real.sqrt,

Goal state after:
x y : ℝ
h : x ≤ y
⊢ ↑(NNReal.sqrt x.toNNReal) ≤ ↑(NNReal.sqrt y.toNNReal)
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ √(x * y) = √x * √y

Tactic:
Real.sqrt,

Goal state after:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ ↑(NNReal.sqrt (x * y).toNNReal) = ↑(NNReal.sqrt x.toNNReal) * ↑(NNReal.sqrt y.toNNReal)
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
⊢ √x⁻¹ = (√x)⁻¹

Tactic:
Real.sqrt,

Goal state after:
x : ℝ
⊢ ↑(NNReal.sqrt x⁻¹.toNNReal) = (√x)⁻¹
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: x : ℝ
hx : x ∈ Ici 0
⊢ √x * √x = x

Tactic:
Real.mul_self_sqrt hx

Goal state after:
x : ℝ
hx : x ∈ Ici 0
⊢ x = x
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
s : Set α
hs : MeasurableSet s
hμs : μ {a | ¬s.indicator f a = 0 a} = 0
⊢ μ s = 0

Tactic:
simp only [ae_iff, ne_eq, not_not] at hf_ne_zero

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
s : Set α
hs : MeasurableSet s
hμs : μ {a | ¬s.indicator f a = 0 a} = 0
hf_ne_zero : μ {a | f a = 0} = 0
⊢ μ s = 0
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: x : ℝ
hx : ‖x‖ ≤ 1
⊢ ‖-x‖ ≤ 1

Tactic:
by simpa

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

Goal state before:
pp: ⊢ ↑0 = 0

Tactic:
by ext <;> simp

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

Goal state before:
pp: z w : ℂ
⊢ ¬z ≤ w ↔ w.re < z.re ∨ z.im ≠ w.im

Tactic:
le_def,

Goal state after:
z w : ℂ
⊢ ¬(z.re ≤ w.re ∧ z.im = w.im) ↔ w.re < z.re ∨ z.im ≠ w.im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: x✝ : ℕ
⊢ ↑(x✝ + 1) = ↑x✝ + 1

Tactic:
by ext <;> simp

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

Goal state before:
pp: x✝ : ℕ
⊢ IntCast.intCast ↑x✝ = ↑x✝

Tactic:
by ext <;> simp

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

Goal state before:
pp: x✝ : ℕ
⊢ IntCast.intCast (Int.negSucc x✝) = -↑(x✝ + 1)

Tactic:
by ext <;> simp

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

Goal state before:
pp: ι : 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
f : ι → M
s : Finset ι
m : M → N
h_mul : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs : s.Nonempty
⊢ ∀ (a b : M), True → True → m (a + b) ≤ m a + m b

Tactic:
by simpa

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

Goal state before:
pp: ι : 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
f : ι → M
s : Finset ι
m : M → N
h_mul : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs : s.Nonempty
⊢ ∀ (n : ℕ) (a : M), True → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a

Tactic:
by simpa

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

Goal state before:
pp: ι : 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
f : ι → M
s : Finset ι
h_zero : m 0 = 0
h_add : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
⊢ ∀ (a b : M), True → True → m (a + b) ≤ m a + m b

Tactic:
by simpa

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

Goal state before:
pp: ι : 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
f : ι → M
s : Finset ι
h_zero : m 0 = 0
h_add : ∀ (a b : M), m (a + b) ≤ m a + m b
h_div : ∀ (n : ℕ) (a : M), m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
⊢ ∀ (n : ℕ) (a : M), True → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a

Tactic:
by simpa

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

Goal state before:
pp: E : Type u_2
inst✝¹ : NonUnitalNormedRing E
inst✝ : StarRing E
h : ∀ (x : E), ‖x‖ * ‖x‖ ≤ ‖x * x⋆‖
this : NormedStarGroup E
⊢ ∀ (x : E), ‖x⋆‖ * ‖x⋆‖ ≤ ‖x⋆⋆ * x⋆‖

Tactic:
by simpa

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

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
x y : ℂ
⊢ (r • (x + y)).re = (r • x + r • y).re

Tactic:
simp [smul_re, smul_im, smul_add]

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

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
x y : ℂ
⊢ (r • (x + y)).im = (r • x + r • y).im

Tactic:
simp [smul_re, smul_im, smul_add]

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

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
⊢ 1 + z ∈ Metric.ball 1 1

Tactic:
by simpa

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
hI : I ≠ 0
⊢ ‖I‖ = 1

Tactic:
← mul_self_inj_of_nonneg (norm_nonneg I) zero_le_one,

Goal state after:
K : Type u_1
inst✝ : RCLike K
hI : I ≠ 0
⊢ ‖I‖ * ‖I‖ = 1 * 1
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case mp
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
⊢ f =o[l] g → ∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖f x‖ ≤ ‖g x‖

pp: case mpr
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
⊢ (∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖f x‖ ≤ ‖g x‖) → f =o[l] g

Tactic:
· rintro H (_ | n)
    · refine (H.def one_pos).mono fun x h₀' => ?_
      rw [Nat.cast_zero, zero_mul]
      refine h₀.elim (fun hf => (hf x).trans ?_) fun hg => hg x
      rwa [one_mul] at h₀'
    · have : (0 : ℝ) < n.succ := Nat.cast_pos.2 n.succ_pos
      exact (isBigOWith_inv this).1 (H.def' <| inv_pos.2 this)

Goal state after:
case mpr
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
⊢ (∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖f x‖ ≤ ‖g x‖) → f =o[l] g
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₂
⊢ (fun x ↦ f₁ x + f₂ x) =O[l] fun x ↦ ‖g₁ x‖ + ‖g₂ x‖

Tactic:
obtain ⟨c₁, hc₁⟩ := h₁.isBigOWith
  obtain ⟨c₂, hc₂⟩ := h₂.isBigOWith
  exact (hc₁.add_add hc₂).isBigO

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

Goal state before:
pp: α : Type u_1
R : Type u_13
inst✝³ : SeminormedRing R
S : Type u_17
inst✝² : NormedRing S
inst✝¹ : NormMulClass S
c : ℝ
l : Filter α
inst✝ : NormOneClass S
f : α → R
g : α → S
h : IsBigOWith c l f g
⊢ IsBigOWith (Nat.casesOn 1 ‖1‖ fun n ↦ c ^ (n + 1)) l (fun x ↦ f x ^ 1) fun x ↦ g x ^ 1

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : NormedDivisionRing 𝕜'
c : ℝ
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsBigOWith c l f g
h₀✝ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
x : α
h₀ : f x = 0 → g x = 0
hle : ‖f x‖ ≤ c * ‖g x‖
⊢ ‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖

Tactic:
rcases eq_or_ne (f x) 0 with hx | hx

Goal state after:
case inl
α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : NormedDivisionRing 𝕜'
c : ℝ
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsBigOWith c l f g
h₀✝ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
x : α
h₀ : f x = 0 → g x = 0
hle : ‖f x‖ ≤ c * ‖g x‖
hx : f x = 0
⊢ ‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖

case inr
α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : NormedDivisionRing 𝕜'
c : ℝ
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsBigOWith c l f g
h₀✝ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
x : α
h₀ : f x = 0 → g x = 0
hle : ‖f x‖ ≤ c * ‖g x‖
hx : f x ≠ 0
⊢ ‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: ⊢ cexp 0 = 1

Tactic:
by
  rw [exp]
  refine lim_eq_of_equiv_const fun ε ε0 => ⟨1, fun j hj => ?_⟩
  convert ε0.lt
  rcases j with - | j
  · exact absurd hj (not_le_of_gt zero_lt_one)
  · dsimp [exp']
    induction j with
    | zero => simp
    | succ j ih =>
      rw [← ih (by simp)]
      simp only [sum_range_succ, pow_succ]
      simp

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

Goal state before:
pp: x : ℂ
n : ℕ
⊢ cexp (↑n.succ * x) = cexp x ^ n.succ

Tactic:
rw [pow_succ, Nat.cast_add_one, add_mul, exp_add, ← exp_nat_mul _ n, one_mul]

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

Goal state before:
pp: x : ℂ
n : ℕ
⊢ cexp (↑n.succ * x) = cexp x ^ n.succ

Tactic:
by rw [pow_succ, Nat.cast_add_one, add_mul, exp_add, ← exp_nat_mul _ n, one_mul]

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

Goal state before:
pp: x : ℂ
⊢ cos (-x) = cos x

Tactic:
by simp [cos, exp_neg, add_comm]

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

Goal state before:
pp: 𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
m p : ℕ
hp0 : 0 < p
h : m < m + p
this : (fun x ↦ x ^ m * x ^ p) =o[𝓝 0] fun x ↦ x ^ m * 1 ^ p
⊢ (fun x ↦ x ^ (m + p)) =o[𝓝 0] fun x ↦ x ^ m

Tactic:
by
    simpa only [pow_add, one_pow, mul_one]

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

Goal state before:
pp: case calc_2
x y : ℂ
⊢ cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) =
    cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2))

pp: case calc_3
x y : ℂ
⊢ cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) =
    2 * cos ((x + y) / 2) * cos ((x - y) / 2)

Tactic:
· rw [cos_add, cos_sub]

Goal state after:
case calc_3
x y : ℂ
⊢ cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) =
    2 * cos ((x + y) / 2) * cos ((x - y) / 2)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖-x * I‖ ≤ 1

Tactic:
by simpa

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

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖x * I‖ ≤ 1

Tactic:
by simpa

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

Goal state before:
pp: x : ℝ
hx : |x| ≤ 1
⊢ ‖↑x‖ ≤ 1

Tactic:
by simpa

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

Goal state before:
pp: x : ℝ
hx0 : 0 < x
hx : x ≤ 2
⊢ x ≤ 1 * 2

Tactic:
by simpa

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

Goal state before:
pp: ⊢ Filter.map Subtype.val (Filter.map (⇑expOrderIso) atTop) = atTop

Tactic:
OrderIso.map_atTop,

Goal state after:
⊢ Filter.map Subtype.val atTop = atTop
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
⊢ cos (π / 2 - x) = sin x

Tactic:
rw [← cos_neg, neg_sub, cos_sub_pi_div_two]

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
m : M
ε : ℝ
hε : 0 < ε
n : M
hn : ↑n = (mk' S) m
hn' : ‖n‖ < ‖(mk' S) m‖ + ε
⊢ ‖m * (m⁻¹ * n)‖ < ‖(mk' S) m‖ + ε

Tactic:
by simpa

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

Goal state before:
pp: n : ℕ
⊢ cos (π / 2 ^ (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2

Tactic:
have A : (1 : ℝ) < 2 ^ (n + 1) := one_lt_pow₀ one_lt_two n.succ_ne_zero
    have B : π / 2 ^ (n + 1) < π := div_lt_self pi_pos A
    have C : 0 < π / 2 ^ (n + 1) := by positivity
    rw [pow_succ, div_mul_eq_div_div, cos_half, cos_pi_over_two_pow n, sqrtTwoAddSeries,
      add_div_eq_mul_add_div, one_mul, ← div_mul_eq_div_div, sqrt_div, sqrt_mul_self] <;>
      linarith [sqrtTwoAddSeries_nonneg le_rfl n]

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

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

Tactic:
trans sin (π / 2 ^ 3)

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

⊢ sin (π / 2 ^ 3) = √(2 - √2) / 2
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)
y : E
hy : y ∈ (fun x_1 ↦ -x + x_1) ⁻¹' (r • s)
⊢ ∃ z ∈ s, r • z = -x + y

Tactic:
simpa [mem_smul_set] using hy

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 y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : Disjoint (closedBall x δ) (closedBall y ε)
hxy : dist x y ≤ ε + δ
⊢ False

Tactic:
obtain ⟨z, hxz, hzy⟩ := exists_dist_le_le hδ hε hxy

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : Disjoint (closedBall x δ) (closedBall y ε)
hxy : dist x y ≤ ε + δ
z : E
hxz : dist x z ≤ δ
hzy : dist z y ≤ ε
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℂ
⊢ cos (↑π / 2 - x) = sin x

Tactic:
rw [← cos_neg, neg_sub, cos_sub_pi_div_two]

Goal state after:
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
r : X
f : C(Y, Z)
K : Set Y
hK : IsCompact K
U : Set (X × Z)
hU : IsOpen[instTopologicalSpaceProd] U
H : MapsTo (⇑((const Y (r, f).1).prodMk (r, f).2)) K U
V : Set X
W : Set Z
hV : IsOpen[inst✝²] V
hW : IsOpen[inst✝] W
hrV : {r} ⊆ V
hKW : ⇑f '' K ⊆ W
hVW : V ×ˢ W ⊆ U
⊢ ∀ x ∈ V ×ˢ {x | (fun g ↦ MapsTo (⇑g) K W) x}, MapsTo (⇑((const Y x.1).prodMk x.2)) K U

Tactic:
rintro ⟨r', f'⟩ ⟨hr'V, hf'⟩ x hxK

Goal state after:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
r : X
f : C(Y, Z)
K : Set Y
hK : IsCompact K
U : Set (X × Z)
hU : IsOpen[instTopologicalSpaceProd] U
H : MapsTo (⇑((const Y (r, f).1).prodMk (r, f).2)) K U
V : Set X
W : Set Z
hV : IsOpen[inst✝²] V
hW : IsOpen[inst✝] W
hrV : {r} ⊆ V
hKW : ⇑f '' K ⊆ W
hVW : V ×ˢ W ⊆ U
r' : X
f' : C(Y, Z)
hr'V : (r', f').1 ∈ V
hf' : (r', f').2 ∈ {x | (fun g ↦ MapsTo (⇑g) K W) x}
x : Y
hxK : x ∈ K
⊢ ((const Y (r', f').1).prodMk (r', f').2) x ∈ U
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
⊢ (if h : ↑(σ t) ≤ 1 / 2 then γ ⟨2 * ↑(σ t), ⋯⟩ else γ' ⟨2 * ↑(σ t) - 1, ⋯⟩) =
    if h : ↑t ≤ 1 / 2 then γ' (σ ⟨2 * ↑t, ⋯⟩) else γ (σ ⟨2 * ↑t - 1, ⋯⟩)

Tactic:
split_ifs with h h₁ h₂

Goal state after:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h : ↑(σ t) ≤ 1 / 2
h₁ : ↑t ≤ 1 / 2
⊢ γ ⟨2 * ↑(σ t), ⋯⟩ = γ' (σ ⟨2 * ↑t, ⋯⟩)

case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h : ↑(σ t) ≤ 1 / 2
h₁ : ¬↑t ≤ 1 / 2
⊢ γ ⟨2 * ↑(σ t), ⋯⟩ = γ (σ ⟨2 * ↑t - 1, ⋯⟩)

case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h : ¬↑(σ t) ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ γ' ⟨2 * ↑(σ t) - 1, ⋯⟩ = γ' (σ ⟨2 * ↑t, ⋯⟩)

case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h : ¬↑(σ t) ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ γ' ⟨2 * ↑(σ t) - 1, ⋯⟩ = γ (σ ⟨2 * ↑t - 1, ⋯⟩)
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: ι : Type u_3
Z : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (Z i)
s : (i : ι) → Set (Z i)
x : (i : ι) → Z i
hx : ∀ (i : ι), x i ∈ s i
hjoin : ∀ (i : ι) ⦃y : Z i⦄, y ∈ s i → JoinedIn (s i) (x i) y
⊢ x ∈ univ.pi s

Tactic:
by simpa

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

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
F : Set X
Z : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (Z i)
inst✝ : ∀ (i : ι), PathConnectedSpace (Z i)
⊢ PathConnectedSpace ((i : ι) → Z i)

Tactic:
rw [pathConnectedSpace_iff_univ, ← Set.pi_univ]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y z : X
ι : Type u_3
F : Set X
Z : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (Z i)
inst✝ : ∀ (i : ι), PathConnectedSpace (Z i)
⊢ IsPathConnected (Set.pi ?m.12 fun i ↦ univ)

X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x y z : X
ι : Type u_3
F : Set X
Z : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (Z i)
inst✝ : ∀ (i : ι), PathConnectedSpace (Z i)
⊢ Set ι
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a : X
⊢ (refl a).trans (refl a) = refl a

Tactic:
by
  ext
  simp [Path.trans]

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

Goal state before:
pp: a : ℝ
⊢ Tendsto (⇑(zmultiples a).subtype) Filter.cofinite (cocompact ℝ)

Tactic:
refine (zmultiples a).tendsto_coe_cofinite_of_discrete ?_
  rw [SetLike.isDiscrete_iff_discreteTopology]
  infer_instance

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

Goal state before:
pp: x✝ y x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
⊢ sin x ∈ Icc (-1) 1

Tactic:
simpa [← abs_le] using abs_sin_le_one x

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

Goal state before:
pp: ψ θ : ℝ
⊢ ↑ψ = ↑θ ↔ ∃ k, θ - ψ = 2 * π * ↑k

Tactic:
QuotientAddGroup.eq

Goal state after:
ψ θ : ℝ
⊢ -ψ + θ ∈ AddSubgroup.zmultiples (2 * π) ↔ ∃ k, θ - ψ = 2 * π * ↑k
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ -↑π = ↑π

Tactic:
neg_coe_pi

Goal state after:
⊢ ↑π = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ + -↑π = θ + ↑π

Tactic:
neg_coe_pi

Goal state after:
θ : Angle
⊢ θ + ↑π = θ + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
left
      rw [eq_div_iff_mul_eq (two_ne_zero' ℝ), eq_sub_iff_add_eq] at hn
      rw [← hn, coe_add, mul_assoc, intCast_mul_eq_zsmul, mul_comm, coe_two_pi, zsmul_zero,
        zero_add]

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

Goal state before:
pp: x : ℂ
hi : x.im < 0
⊢ (-x).arg = x.arg + π

Tactic:
by
  rw [arg_of_im_neg hi, arg_of_im_pos (show 0 < (-x).im from Left.neg_pos_iff.2 hi)]
  simp [neg_div, Real.arccos_neg, add_comm, ← sub_eq_add_neg]

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

Goal state before:
pp: ⊢ (↑π).toReal = π

Tactic:
rw [toReal_coe_eq_self_iff]
  exact ⟨Left.neg_lt_self Real.pi_pos, le_refl _⟩

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

Goal state before:
pp: 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

Tactic:
· rw [arg_ofReal_of_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr)]
      simp [hr]

Goal state after:
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:
rw [mul_assoc, mul_comm (exp _), ← mul_assoc (‖y‖ : ℂ), norm_mul_exp_arg_mul_I, mul_comm y, ←
    mul_assoc, norm_mul_exp_arg_mul_I]

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

Goal state before:
pp: θ : Angle
| θ.tan

Tactic:
rw [← coe_toReal θ, tan_coe]

Goal state after:
θ : Angle
| Real.tan θ.toReal