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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
inst✝¹ : SFinite μb
inst✝ : SFinite μc
s : Set (α × β × γ)
hs : MeasurableSet s
A : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)
B : MeasurableSet (⇑MeasurableEquiv.prodAssoc ⁻¹' s)
⊢ (map (⇑MeasurableEquiv.prodAssoc) ((μa.prod μb).prod μc)) s = (μa.prod (μb.prod μc)) s

Tactic:
simp_rw [map_apply MeasurableEquiv.prodAssoc.measurable hs, Measure.prod_apply hs,
    Measure.prod_apply (A _), Measure.prod_apply B,
    lintegral_prod _ (measurable_measure_prodMk_left B).aemeasurable]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
inst✝¹ : SFinite μb
inst✝ : SFinite μc
s : Set (α × β × γ)
hs : MeasurableSet s
A : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)
B : MeasurableSet (⇑MeasurableEquiv.prodAssoc ⁻¹' s)
⊢ ∫⁻ (x : α), ∫⁻ (y : β), μc (Prod.mk (x, y) ⁻¹' ⇑MeasurableEquiv.prodAssoc ⁻¹' s) ∂μb ∂μa =
    ∫⁻ (x : α), ∫⁻ (x_1 : β), μc (Prod.mk x_1 ⁻¹' Prod.mk x ⁻¹' s) ∂μb ∂μa
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x | f x = 0}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᵐ[μ] g
a : α
ha : f a = 0
h : {x | g x = 0} a
⊢ {x | f x = 0} a

Tactic:
exact ha

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
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
hs : MeasurableSet s
t : Set G
ht : MeasurableSet t
h1 :
  ν' s * ∫⁻ (y : G), t.indicator (fun x ↦ 1) y⁻¹ / ν' ((fun x ↦ x * y⁻¹) ⁻¹' s) ∂ν' =
    ∫⁻ (x : G), t.indicator (fun x ↦ 1) x ∂ν'
⊢ μ' s * ν' t = ν' s * μ' t

Tactic:
have h2 := measure_lintegral_div_measure μ' ν' hs h2s h3s (t.indicator fun _ => 1)
    (measurable_const.indicator ht)

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
hs : MeasurableSet s
t : Set G
ht : MeasurableSet t
h1 :
  ν' s * ∫⁻ (y : G), t.indicator (fun x ↦ 1) y⁻¹ / ν' ((fun x ↦ x * y⁻¹) ⁻¹' s) ∂ν' =
    ∫⁻ (x : G), t.indicator (fun x ↦ 1) x ∂ν'
h2 :
  μ' s * ∫⁻ (y : G), t.indicator (fun x ↦ 1) y⁻¹ / ν' ((fun x ↦ x * y⁻¹) ⁻¹' s) ∂ν' =
    ∫⁻ (x : G), t.indicator (fun x ↦ 1) x ∂μ'
⊢ μ' s * ν' t = ν' s * μ' t
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: r : ℝ
⊢ ↑‖↑r‖₊ = ↑‖r‖₊

Tactic:
exact norm_real _

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

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

Tactic:
by
  rw [restrict_withDensity hs, lintegral_withDensity_eq_lintegral_mul_non_measurable _ f_meas hf]

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

Goal state before:
pp: z : ℂ
⊢ -z.re = ‖z‖ ↔ z ≤ 0

Tactic:
rw [← neg_re, ← norm_neg z, re_eq_norm]

Goal state after:
z : ℂ
⊢ 0 ≤ -z ↔ z ≤ 0
Module: Mathlib.Data.Complex.Basic

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

Tactic:
by simp [mul_assoc]

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₂
x✝ : V₁
⊢ ‖0 x✝‖ = 0 * ‖x✝‖

Tactic:
rw [zero_mul]
            exact norm_zero

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

Goal state before:
pp: V₁ : Type u_3
V₂ : Type u_4
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
⊢ (f.comp (incl ⊤)).range = f.range

Tactic:
simp [comp_range, incl_range, ← AddMonoidHom.range_eq_map]

Goal state after:
V₁ : Type u_3
V₂ : Type u_4
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
⊢ f.toAddMonoidHom.range = f.range
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
U : ↥(unitary E)
⊢ ‖↑U‖ * ‖↑U‖ = 1

Tactic:
← CStarRing.norm_star_mul_self,

Goal state after:
E : Type u_2
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CStarRing E
inst✝ : Nontrivial E
U : ↥(unitary E)
⊢ ‖(↑U)⋆ * ↑U‖ = 1
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r : ℂ
⊢ (0 • r).re = re 0

Tactic:
simp [smul_re, smul_im, zero_smul]

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

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r : ℂ
⊢ (0 • r).im = im 0

Tactic:
simp [smul_re, smul_im, zero_smul]

Goal state after:
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
⊢ star x * x - x * star x = 0 ↔ Commute ↑(ℜ x) ↑(ℑ x)

Tactic:
star_mul_self_sub_self_mul_star,

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
⊢ 2 • I • (↑(ℜ x) * ↑(ℑ x) - ↑(ℑ x) * ↑(ℜ x)) = 0 ↔ Commute ↑(ℜ x) ↑(ℑ x)
Module: Mathlib.Analysis.RCLike.Basic

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

Tactic:
by
  rw [← ofReal_nnratCast]; exact norm_of_nonneg q.cast_nonneg

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

Goal state before:
pp: case h
X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
x : Y
hx : x ∈ range f
⊢ x ∈ (toPartialHomeomorph f h).target

Tactic:
rwa [toPartialHomeomorph_target]

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝ : RCLike K
z : K
h : ‖z‖ ≤ re z
⊢ z = ↑‖z‖

Tactic:
have h' : ‖z‖ = re z := (le_antisymm (re_le_norm z) h).symm
    rw [h', re_eq_self_of_le h]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ im z ≤ -‖z‖ ↔ z = -(I * ↑‖z‖)

Tactic:
simpa [neg_eq_iff_eq_neg, le_neg] using norm_le_im_iff_eq_I_mul_norm (z := -z)

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

Goal state before:
pp: 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)⁻¹‖

Tactic:
simp only [hx, h₀ hx, inv_zero, norm_zero, mul_zero, le_rfl]

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

Goal state before:
pp: case cons
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
s✝ : Finset ι
B : ι → α → ℝ
i : ι
s : Finset ι
his : i ∉ s
h : (∀ i ∈ s, A i =o[l] B i) → (fun H ↦ ∑ i ∈ s, A i H) =o[l] fun H ↦ ∑ i ∈ s, ‖B i H‖
hAB : ∀ i_1 ∈ Finset.cons i s his, A i_1 =o[l] B i_1
⊢ (fun H ↦ A i H + ∑ i ∈ s, A i H) =o[l] fun H ↦ ‖B i H‖ + ∑ i ∈ s, ‖B i H‖

Tactic:
calc (fun H => A i H + ∑ j ∈ s, A j H)
      =o[l] fun H => ‖B i H‖ + ‖∑ j ∈ s, ‖B j H‖‖ :=
          (hAB i (by simp)).add_add (h (fun j hj => hAB j (by simp [hj])))
    _ =ᶠ[l] fun H => ‖B i H‖ + ∑ j ∈ s, ‖B j H‖ := by
        refine Eventually.of_forall fun H ↦ congr_arg (‖B i H‖ + ·) ?_
        exact Real.norm_of_nonneg (Finset.sum_nonneg fun _ _ => norm_nonneg _)

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

Goal state before:
pp: case nil
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
hf : ∀ i ∈ [], f i =O[l] g i
⊢ (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) []).prod) =O[l] fun x ↦ (List.map (fun x_1 ↦ g x_1 x) []).prod

Tactic:
simp [isBoundedUnder_const]

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

Goal state before:
pp: 𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
h : f =O[l] g
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f x / g x‖

Tactic:
by
  obtain ⟨c, h₀, hc⟩ := h.exists_nonneg
  refine ⟨c, eventually_map.2 (hc.bound.mono fun x hx => ?_)⟩
  rw [norm_div]
  exact div_le_of_le_mul₀ (norm_nonneg _) h₀ hx

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

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

Tactic:
rw [← add_div, add_sub, add_right_comm, add_sub_cancel_right, add_self_div_two] at s1

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

Goal state before:
pp: x y : ℂ
s1 : cos ((x + y) / 2 + (x - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)
s2 : 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 - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2)

Tactic:
rw [← add_div, add_sub, add_right_comm, add_sub_cancel_right, add_self_div_two] at s1

Goal state after:
x y : ℂ
s1 : cos x = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)
s2 : 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 - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cos x ^ 2 = 1 - sin x ^ 2

Tactic:
← sin_sq_add_cos_sq x,

Goal state after:
x : ℂ
⊢ cos x ^ 2 = sin x ^ 2 + cos x ^ 2 - sin x ^ 2
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ sin x ^ 2 = 1 - cos x ^ 2

Tactic:
← sin_sq_add_cos_sq x,

Goal state after:
x : ℂ
⊢ sin x ^ 2 = sin x ^ 2 + cos x ^ 2 - cos x ^ 2
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
h : cos x ≠ 0
| 1

Tactic:
← sin_sq_add_cos_sq x,

Goal state after:
x : ℂ
h : cos x ≠ 0
| sin x ^ 2 + cos x ^ 2
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
rw [← two_add_one_eq_three, add_one_mul, sin_add (2 * x) x]
  simp only [cos_two_mul, sin_two_mul, cos_sq', mul_assoc, ← sq]
  ring

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

Goal state before:
pp: x : ℝ
⊢ cos x ^ 2 = 1 - sin x ^ 2

Tactic:
← sin_sq_add_cos_sq x,

Goal state after:
x : ℝ
⊢ cos x ^ 2 = sin x ^ 2 + cos x ^ 2 - sin x ^ 2
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:

Tactic:
0 < x - x ^ 3 / 6 - |x| ^ 5 / 100 := by grind [pow_le_of_le_one]
    _ ≤ sin x :=
      sub_le_comm.1 (abs_sub_le_iff.1 (sin_bound (by rwa [abs_of_nonneg (le_of_lt hx0)]))).2

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : OpenPartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
C : ℝ
h : IsBigOWith C (𝓝 b) f g
this : ContinuousAt (↑e) (↑e.symm b)
⊢ Tendsto (↑e) (𝓝 (↑e.symm b)) (𝓝 b)

Tactic:
rwa [ContinuousAt, e.rightInvOn hb] at this

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

Goal state before:
pp: a : ℝ
⊢ UniformContinuousOn cexp {x | x.re ≤ a}

Tactic:
have : Continuous (cexp - 1) := Continuous.sub (by fun_prop) continuous_one

Goal state after:
a : ℝ
this : Continuous (cexp - 1)
⊢ UniformContinuousOn cexp {x | x.re ≤ a}
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
n m : ℕ
hmn : n.succ ≤ m
hr0 : 0 ≤ 0
hr1 : 0 < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ 0 * abv (f m)
har1 : |0| < 1
⊢ abv (f m) ≤ abv (f n.succ) * 0⁻¹ ^ n.succ * 0 ^ m

Tactic:
have m_pos := lt_of_lt_of_le (Nat.succ_pos n) hmn
    have := h m.pred (Nat.le_of_succ_le_succ (by rwa [Nat.succ_pred_eq_of_pos m_pos]))
    simpa [Nat.sub_add_cancel m_pos, pow_succ] using this

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‖ < ε}
⊢ (Filter.map mk (𝓝 1)).HasBasis (fun ε ↦ 0 < ε) fun ε ↦ {x | ‖x‖ < ε}

Tactic:
← funext this

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 ↦ mk '' ball 1 x
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
x : E
⊢ s * ball x δ = x • thickening δ s

Tactic:
mul_ball

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
x : E
⊢ x • thickening δ s = x • thickening δ s
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
⊢ frontier (closedBall x r) = sphere x r

Tactic:
rw [frontier, closure_closedBall, interior_closedBall x hr, closedBall_sdiff_ball]

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

Goal state before:
pp: case neg
k : ℕ
r : ℝ
hr : |r| < 1
h0 : ¬r = 0
⊢ Tendsto (fun n ↦ ↑n ^ k * r ^ n) atTop (𝓝 0)

Tactic:
have hr' : 1 < |r|⁻¹ := (one_lt_inv₀ (abs_pos.2 h0)).2 hr

Goal state after:
case neg
k : ℕ
r : ℝ
hr : |r| < 1
h0 : ¬r = 0
hr' : 1 < |r|⁻¹
⊢ Tendsto (fun n ↦ ↑n ^ k * r ^ n) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ Function.Antiperiodic (fun x ↦ cexp (x * I)) ↑π

Tactic:
simpa only [mul_inv_cancel_right₀ I_ne_zero] using exp_antiperiodic.mul_const I_ne_zero

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
⊢ ⨅ b ∈ {K | IsCompact K} ×ˢ {t | IsOpen[inst✝] t}, ⨅ (_ : f ∈ {f | MapsTo (⇑f) b.1 b.2}), 𝓟 {f | MapsTo (⇑f) b.1 b.2} =
    ⨅ K, ⨅ (_ : IsCompact K), ⨅ U, ⨅ (_ : IsOpen[inst✝] U), ⨅ (_ : MapsTo (⇑f) K U), 𝓟 {g | MapsTo (⇑g) K U}

Tactic:
biInf_prod,

Goal state after:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
⊢ ⨅ a ∈ {K | IsCompact K}, ⨅ b ∈ {t | IsOpen[inst✝] t}, ⨅ (_ : f ∈ {f | MapsTo (⇑f) a b}), 𝓟 {f | MapsTo (⇑f) a b} =
    ⨅ K, ⨅ (_ : IsCompact K), ⨅ U, ⨅ (_ : IsOpen[inst✝] U), ⨅ (_ : MapsTo (⇑f) K U), 𝓟 {g | MapsTo (⇑g) K U}
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
⊢ 𝓝 f = ⨅ s, ⨅ (_ : IsCompact s), comap (restrict s) (𝓝 (restrict s f))

Tactic:
simp only [nhds_iInf, nhds_induced]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Real

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
⊢ toAddCircle j = ↑(↑j.val / ↑N)

Tactic:
rw [← toAddCircle_natCast, natCast_zmod_val]

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ₂
h₁' : Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ₁ t).extend
h₂' : Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ₂ t).extend
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ (γ₁ t).trans (γ₂ t)

Tactic:
simp only [HasUncurry.uncurry, Path.trans]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ₂
h₁' : Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ₁ t).extend
h₂' : Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ₂ t).extend
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦
    { toFun := (fun t ↦ if t ≤ 1 / 2 then (γ₁ p.1).extend (2 * t) else (γ₂ p.1).extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
      p.2
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
⊢ range ⇑(γ.truncate t₀ t₁) ⊆ range ⇑γ

Tactic:
by
  rw [← γ.extend_range]
  simp only [range_subset_iff, SetCoe.forall]
  intro x _hx
  simp only [DFunLike.coe, Path.truncate, mem_range_self]

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

Goal state before:
pp: x : ℝ
⊢ arcsin x = 0 ↔ x = 0

Tactic:
by simp [le_antisymm_iff]

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

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ log x⁻¹

Tactic:
apply log_nonneg

Goal state after:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 1 ≤ x⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ ↑π + ↑π = 0

Tactic:
by rw [← two_nsmul, two_nsmul_coe_pi]

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

Goal state before:
pp: x : ℂ
hx : 0 ≤ x.im
x✝ : ∃ n, x = ↑n * (2 * ↑π * I)
n : ℕ
hn : x = ↑n * (2 * ↑π * I)
⊢ x = ↑↑n * (2 * ↑π * I)

Tactic:
rw [hn]

Goal state after:
x : ℂ
hx : 0 ≤ x.im
x✝ : ∃ n, x = ↑n * (2 * ↑π * I)
n : ℕ
hn : x = ↑n * (2 * ↑π * I)
⊢ ↑n * (2 * ↑π * I) = ↑↑n * (2 * ↑π * I)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x a : ℂ
⊢ 0 ^ x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
by
  constructor
  · intro hyp
    simp only [cpow_def, if_true] at hyp
    grind
  · rintro (⟨h, rfl⟩ | ⟨rfl, rfl⟩)
    · exact zero_cpow h
    · exact cpow_zero _

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

Goal state before:
pp: θ : ℝ
⊢ (↑1 * (cos ↑θ + sin ↑θ * I)).arg = toIocMod Real.two_pi_pos (-π) θ

Tactic:
arg_mul_cos_add_sin_mul_I_eq_toIocMod zero_lt_one

Goal state after:
θ : ℝ
⊢ toIocMod Real.two_pi_pos (-π) θ = toIocMod Real.two_pi_pos (-π) θ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case h
r : ℝ
hr : 0 < r
θ : ℝ
⊢ ↑(↑r * (↑(↑θ).cos + ↑(↑θ).sin * I)).arg = ↑θ

Tactic:
| _ θ
   => 

Goal state after:
case h
r : ℝ
hr : 0 < r
θ : ℝ
⊢ ↑(↑r * (↑(↑θ).cos + ↑(↑θ).sin * I)).arg = ↑θ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
← mul_assoc (‖y‖ : ℂ),

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

Goal state before:
pp: a b c : ℝ
hb : 0 ≠ b
⊢ Tendsto ?m.40 atTop (𝓝 0)

Tactic:
by
              simpa only [mul_zero, pow_one] using
                (tendsto_const_nhds (x := a)).mul
                  (tendsto_div_pow_mul_exp_add_atTop b c 1 hb)

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

Goal state before:
pp: y : ℝ
hp : 0 < y
A : Tendsto (fun p ↦ rexp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
B : Tendsto (fun p ↦ p.1 ^ p.2) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
⊢ Tendsto (fun p ↦ p.1 ^ p.2) (𝓝[{0}] 0 ×ˢ 𝓝 y) (pure 0)

Tactic:
rw [nhdsWithin_singleton, tendsto_pure, pure_prod, eventually_map]

Goal state after:
y : ℝ
hp : 0 < y
A : Tendsto (fun p ↦ rexp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
B : Tendsto (fun p ↦ p.1 ^ p.2) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
⊢ ∀ᶠ (a : ℝ) in 𝓝 y, (0, a).1 ^ (0, a).2 = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: z : ℝ
h : 0 ≤ z
h0 : 0 = z
⊢ Monotone fun x ↦ x ^ 0

Tactic:
simp only [rpow_zero, monotone_const]

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

Goal state before:
pp: case inr.inr.inr
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
h_top : x ≠ ∞
⊢ x⁻¹ ^ y * x ^ y = 1

Tactic:
← mul_rpow_of_ne_zero (ENNReal.inv_ne_zero.2 h_top) h0,

Goal state after:
case inr.inr.inr
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
h_top : x ≠ ∞
⊢ (x⁻¹ * x) ^ y = 1
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ SameRay R (-x) y ↔ SameRay R x (-y)

Tactic:
rw [← sameRay_neg_iff, neg_neg]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case h
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : M ≃ₗ[R] N
g : M
hg : g ≠ 0
⊢ (map f) (-rayOfNeZero R g hg) = -(map f) (rayOfNeZero R g hg)

Tactic:
| h g hg =>

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
f g : P1 →ᵃ[k] P2
h₁ : f.linear = g.linear
p : P1
h₂ : f p = g p
⊢ f = g

Tactic:
by
  ext q
  have hgl : g.linear (q -ᵥ p) = toFun g ((q -ᵥ p) +ᵥ q) -ᵥ toFun g q := by simp
  have := f.map_vadd' q (q -ᵥ p)
  rw [h₁, hgl, toFun_eq_coe, map_vadd, linearMap_vsub, h₂] at this
  simpa

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
p : P
hp : p ∈ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : v = p₁ -ᵥ p₂
⊢ v +ᵥ p ∈ s

Tactic:
hv

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
p : P
hp : p ∈ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : v = p₁ -ᵥ p₂
⊢ (p₁ -ᵥ p₂) +ᵥ p ∈ s