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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
s : Set γ
hs : MeasurableSet s
⊢ (map (fun a ↦ (X a, Y a)) μ).snd s = (map Y μ) s

Tactic:
rw [Measure.snd_apply hs, Measure.map_apply_of_aemeasurable (hX.prodMk hY) (measurable_snd hs),
      Measure.map_apply_of_aemeasurable hY hs, ← univ_prod, mk_preimage_prod, preimage_univ,
      univ_inter]

Goal state after:
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x y : G
| (∫⁻ (y_1 : G), f y_1 * g (y_1⁻¹ * y) ∂μ) * k (y⁻¹ * x)

Tactic:
rw [← lintegral_mul_const'' _ (by fun_prop)]

Goal state after:
G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x y : G
| ∫⁻ (a : G), f a * g (a⁻¹ * y) * k (y⁻¹ * x) ∂μ
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✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulRightInvariant
⊢ QuasiMeasurePreserving (fun p ↦ p.1 / p.2) (μ.prod ν) μ

Tactic:
by
  refine QuasiMeasurePreserving.prod_of_left measurable_div (Eventually.of_forall fun y => ?_)
  exact (measurePreserving_div_right μ y).quasiMeasurePreserving

Goal state after:
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : a < 0
this : Tendsto (fun x ↦ (a * x + b) * x + c) atTop atBot
x : K
hx : (a * x + b) * x + c < 0
⊢ a * (x * x) + b * x + c < 0

Tactic:
rwa [← mul_assoc, ← add_mul]

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
f : α → ε
h : HasFiniteIntegral f μ
c : ℝ≥0∞
hc : c ≠ ∞
⊢ HasFiniteIntegral f (c • μ)

Tactic:
simp only [HasFiniteIntegral, lintegral_smul_measure] at *

Goal state after:
α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
f : α → ε
h : ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
c : ℝ≥0∞
hc : c ≠ ∞
⊢ c • ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
Module: Mathlib.Analysis.Real.Sqrt

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

Tactic:
sqrt_le_sqrt_iff zero_le_one,

Goal state after:
x : ℝ
⊢ x ≤ 1 ↔ x ≤ √1
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
⊢ nndist z ((starRingEnd ℂ) z) = 2 * Real.nnabs z.im

Tactic:
by
  rw [nndist_comm, nndist_conj_self]

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

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝³ : Monoid A
inst✝² : Star A
inst✝¹ : Monoid B
inst✝ : Star B
f g : A →⋆* B
h : (fun f ↦ (↑f.toMonoidHom).toFun) f = (fun f ↦ (↑f.toMonoidHom).toFun) g
⊢ f = g

Tactic:
by cases f; cases g; simp_all

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

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝⁷ : Mul A
inst✝⁶ : Mul B
inst✝⁵ : Mul C
inst✝⁴ : Mul D
inst✝³ : Star A
inst✝² : Star B
inst✝¹ : Star C
inst✝ : Star D
f g : A ≃⋆* B
h : f.toFun = g.toFun
⊢ f.invFun = g.invFun → f = g

Tactic:
by cases f; cases g; simp_all

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

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ‖f x‖ ≤ C * ‖x‖
h : ¬‖x‖ = 0
hlt : 0 < ‖x‖
c : ℝ
x✝ : c ∈ {c | 0 ≤ c ∧ ∀ (x : V₁), ‖f x‖ ≤ c * ‖x‖}
left✝ : 0 ≤ c
hc : ∀ (x : V₁), ‖f x‖ ≤ c * ‖x‖
⊢ ‖f x‖ ≤ c * ‖x‖

Tactic:
apply hc

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ im 1 = 0

Tactic:
by rw [← ofReal_one, ofReal_im]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hI' : I' * I' = -1
⊢ (liftAux I' hI').range = ℝ[I']

Tactic:
← Algebra.map_top,

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hI' : I' * I' = -1
⊢ Subalgebra.map (liftAux I' hI') ⊤ = ℝ[I']
Module: Mathlib.Analysis.Asymptotics.Theta

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ f =Θ[l ×ˢ l'] g → ∀ᶠ (y : β) in l', (fun x ↦ f (x, y)) =Θ[l] fun x ↦ g (x, y)

Tactic:
simp only [IsTheta, eventually_and]
  exact fun ⟨h₁, h₂⟩ ↦ ⟨h₁.fiberwise_left, h₂.fiberwise_left⟩

Goal state after:
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: n : ℕ
pn : NormNum.IsNat n 0
⊢ Finset.range n = ∅

Tactic:
by rw [pn.out, Nat.cast_zero, Finset.range_zero]

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

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : IsBigOWith c₁ l f₁ g
h₂ : IsBigOWith c₂ l f₂ g
⊢ IsBigOWith (c₁ + c₂) l (fun x ↦ f₁ x - f₂ x) g

Tactic:
by
  simpa only [sub_eq_add_neg] using h₁.add h₂.neg_left

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

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

Tactic:
by
  simpa only [sub_eq_add_neg] using h₁.add h₂.neg_left

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

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

Tactic:
by
  simpa only [sub_eq_add_neg] using h₁.add h₂.neg_left

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

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ
hf : 1 ≤ᶠ[l] f
m n : ℕ
h : n ≤ m
⊢ ∀ᶠ (x : α) in l, ‖(f ^ n) x‖ ≤ 1 * ‖(f ^ m) x‖

Tactic:
exact hf.mono fun x hx ↦ by simp [abs_eq_self.mpr (zero_le_one.trans hx), pow_le_pow_right₀ hx h]

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

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

Tactic:
by rw [← tanh_conj, conj_ofReal]

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

Goal state before:
pp: case pos
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
c : ℝ
hc : ∀ᶠ (a : α) in l, ‖f a‖ / ‖g a‖ ≤ c
x : α
hx₁ : g x = 0 → f x = 0
hx₂ : ‖f x‖ / ‖g x‖ ≤ c
hgx : g x = 0
⊢ ‖f x‖ ≤ c * ‖g x‖

Tactic:
simp [hx₁ hgx, hgx]

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

Goal state before:
pp: x : ℂ
h : I * sin (x * I) = -sinh x
⊢ sin (x * I) = sinh x * I

Tactic:
rw [← neg_neg (sinh x), ← h]

Goal state after:
x : ℂ
h : I * sin (x * I) = -sinh x
⊢ sin (x * I) = -(I * sin (x * I)) * I
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖∑ m ∈ range j, x ^ m / ↑m.factorial - ∑ m ∈ range n, x ^ m / ↑m.factorial‖ ≤
    ∑ m ∈ range j, ‖x‖ ^ m / ↑m.factorial - ∑ m ∈ range n, ‖x‖ ^ m / ↑m.factorial

Tactic:
by
    rw [sum_range_sub_sum_range hj, sum_range_sub_sum_range hj]
    refine (IsAbsoluteValue.abv_sum norm ..).trans_eq ?_
    congr with i
    simp [Complex.norm_pow, Complex.norm_natCast]

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

Goal state before:
pp: α : Type u_1
inst✝² : NormedRing α
inst✝¹ : NormSMulClass ℤ α
inst✝ : Nontrivial α
⊢ Tendsto (fun x ↦ ‖↑x‖) (atBot ⊔ atTop) atTop

Tactic:
simpa [norm_intCast_eq_abs_mul_norm_one] using tendsto_intCast_atTop_atTop
    |>.comp (tendsto_abs_atBot_atTop.sup tendsto_abs_atTop_atTop)
    |>.atTop_mul_const (norm_pos_iff.mpr one_ne_zero)

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
a : M
this✝ : Nonempty ↑{m | ↑m = ↑a}
b : M
this : Nonempty ↑{m | ↑m = ↑b}
⊢ ⨅ y, dist 1 ↑y ≤ dist 1 ↑⟨a, ⋯⟩ + dist 1 ↑⟨b, ⋯⟩

Tactic:
refine ciInf_le_of_le ⟨0, forall_mem_range.2 fun _ ↦ dist_nonneg⟩ ⟨a * b, rfl⟩ ?_

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
a : M
this✝ : Nonempty ↑{m | ↑m = ↑a}
b : M
this : Nonempty ↑{m | ↑m = ↑b}
⊢ dist 1 ↑⟨a * b, ⋯⟩ ≤ dist 1 ↑⟨a, ⋯⟩ + dist 1 ↑⟨b, ⋯⟩
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

Tactic:
by
        rw [← Int.emod_add_mul_ediv n 2, hn1, Int.cast_add, Int.cast_one, add_mul, one_mul,
          add_comm, mul_comm (2 : ℤ), Int.cast_mul, mul_assoc, Int.cast_two] at hn
        rw [← hn, cos_int_mul_two_pi_add_pi] at h
        exact absurd h (by norm_num)

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

Goal state before:
pp: R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n ↦ x ^ n
⊢ ‖∑' (b : ℕ), (fun n ↦ x ^ (n + 1)) b‖ ≤ (1 - ‖x‖)⁻¹ - 1

Tactic:
refine tsum_of_norm_bounded ?_ fun b ↦ norm_pow_le' _ (Nat.succ_pos b)

Goal state after:
R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n ↦ x ^ n
⊢ HasSum (fun b ↦ ‖x‖ ^ (b + 1)) ((1 - ‖x‖)⁻¹ - 1)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
r : ℝ
hr : 0 ≤ r
⊢ 0 • closedBall x r = closedBall (0 • x) (‖0‖ * r)

Tactic:
simp [hr, zero_smul_set, Set.singleton_zero, nonempty_closedBall]

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case refine_2
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : ∃ i, (IsCompact i.1 ∧ p i.2) ∧ {f | MapsTo (⇑f) i.1 (U i.2)} ⊆ s
⊢ s ∈ 𝓝 (const X c)

Tactic:
· rcases hs with ⟨⟨K, i⟩, ⟨hK, hpi⟩, hi⟩
    filter_upwards [eventually_mapsTo hK isOpen_interior fun x _ ↦
      mem_interior_iff_mem_nhds.mpr <| h.mem_of_mem hpi] with f hf
    exact hi <| hf.mono_right interior_subset

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
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
⊢ (∃ f, Tendsto F l (𝓝 f)) ↔ ∀ (s : Set X), IsCompact s → ∃ f, Tendsto (fun i ↦ restrict s (F i)) l (𝓝 f)

Tactic:
constructor
  · rintro ⟨f, hf⟩ s _
    exact ⟨f.restrict s, tendsto_compactOpen_restrict hf s⟩
  · intro h
    choose f hf using h
    -- By uniqueness of limits in a `T2Space`, since `fun i ↦ F i x` tends to both `f s₁ hs₁ x` and
    -- `f s₂ hs₂ x`, we have `f s₁ hs₁ x = f s₂ hs₂ x`
    have h :
      ∀ (s₁) (hs₁ : IsCompact s₁) (s₂) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
        f s₁ hs₁ ⟨x, hxs₁⟩ = f s₂ hs₂ ⟨x, hxs₂⟩ := by
      rintro s₁ hs₁ s₂ hs₂ x hxs₁ hxs₂
      have := isCompact_iff_compactSpace.mp hs₁
      have := isCompact_iff_compactSpace.mp hs₂
      have h₁ := (continuous_eval_const (⟨x, hxs₁⟩ : s₁)).continuousAt.tendsto.comp (hf s₁ hs₁)
      have h₂ := (continuous_eval_const (⟨x, hxs₂⟩ : s₂)).continuousAt.tendsto.comp (hf s₂ hs₂)
      exact tendsto_nhds_unique h₁ h₂
    -- So glue the `f s hs` together and prove that this glued function `f₀` is a limit on each
    -- compact set `s`
    refine ⟨liftCover' _ _ h exists_compact_mem_nhds, ?_⟩
    rw [tendsto_compactOpen_iff_forall]
    intro s hs
    rw [liftCover_restrict']
    exact hf s hs

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
y : Y
s : Set X
⊢ ⇑(coev X Y y) '' s = {y} ×ˢ s

Tactic:
simp [singleton_prod]

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 s : Set X
t : Set Y
inst✝¹ : PathConnectedSpace X
inst✝ : PathConnectedSpace Y
⊢ PathConnectedSpace (X × Y)

Tactic:
rw [pathConnectedSpace_iff_univ, ← Set.univ_prod_univ]
  exact isPathConnected_univ.prod isPathConnected_univ

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

Goal state before:
pp: p x t : ℝ
⊢ ‖↑(t * x)‖ = |t| * ‖↑x‖

Tactic:
by
  obtain rfl | ht := eq_or_ne t 0
  · simp
  simp only [norm_eq_infDist, ← Real.norm_eq_abs, ← infDist_smul₀ ht, smul_zero]
  congr 1 with m
  simp_rw [zmultiples, eq_iff_sub_mem, zsmul_eq_mul, mul_left_comm, ← smul_eq_mul, Set.range_smul]
  simp [mem_smul_set_iff_inv_smul_mem₀ ht, mul_sub, ht]

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

Goal state before:
pp: x y : ℝ
hy₀ : 0 ≤ y
hy₁ : y ≤ π
hxy : x = cos y
⊢ arccos (cos y) = y

Tactic:
arccos_cos hy₀ hy₁

Goal state after:
x y : ℝ
hy₀ : 0 ≤ y
hy₁ : y ≤ π
hxy : x = cos y
⊢ y = y
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
exact le_trans (mul_nonpos_of_nonneg_of_nonpos (by simp only [Nat.ofNat_nonneg]) hx0.le)
      (exp_nonneg x)

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

Goal state before:
pp: z : ℂ
⊢ z.arg = π ↔ z.re < 0 ∧ z.im = 0

Tactic:
by_cases h₀ : z = 0
  · simp [h₀, Real.pi_ne_zero.symm]
  constructor
  · intro h
    rw [← norm_mul_cos_add_sin_mul_I z, h]
    simp [h₀]
  · obtain ⟨x, y⟩ := z
    rintro ⟨h : x < 0, rfl : y = 0⟩
    rw [← arg_neg_one, ← arg_real_mul (-1) (neg_pos.2 h)]
    simp [← ofReal_def]

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

Goal state before:
pp: case inr
x : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ log 1 < log x ↔ 1 < x

Tactic:
exact log_lt_log_iff zero_lt_one hx

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

Goal state before:
pp: ⊢ cobounded ℂ ≤ 𝓟 {0}ᶜ

Tactic:
le_principal_iff

Goal state after:
⊢ {0}ᶜ ∈ cobounded ℂ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

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

pp: case mpr
x a : ℂ
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 → 0 ^ x = a

Tactic:
· intro hyp
    simp only [cpow_def, if_true] at hyp
    grind

Goal state after:
case mpr
x a : ℂ
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 → 0 ^ x = a
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x : ℂ
n : ℕ
⊢ x ^ ↑n = x ^ n

Tactic:
simpa using cpow_nat_mul x n 1

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

Goal state before:
pp: θ : Angle
⊢ θ.toReal ≤ π

Tactic:
induction θ using Real.Angle.induction_on
  convert! toIocMod_le_right two_pi_pos _ _
  ring

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‖) * (cos ↑(x.arg + y.arg) + ↑(Real.sin (x.arg + y.arg)) * I)

Tactic:
ofReal_sin,

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

Goal state before:
pp: θ : Angle
⊢ Real.sin θ.toReal = θ.sin

Tactic:
by
  conv_rhs => rw [← coe_toReal θ, sin_coe]

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

Goal state before:
pp: θ ψ : Angle
h : θ = ↑(π / 2) - ψ ∨ θ = ↑(π / 2) - ψ + ↑π
⊢ |θ.cos| = |ψ.sin|

Tactic:
rcases h with (rfl | rfl) <;> simp [cos_pi_div_two_sub]

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

Goal state before:
pp: b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ (fun x ↦ rexp (log b * x)) =o[atTop] fun _x ↦ 1

Tactic:
rw [isLittleO_const_iff one_ne_zero]

Goal state after:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (fun x ↦ rexp (log b * x)) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case mpr.inl
x : ℝ
h : x ≠ 0
⊢ 0 ^ x = 0

pp: case mpr.inr
⊢ 0 ^ 0 = 1

Tactic:
· exact zero_rpow h

Goal state after:
case mpr.inr
⊢ 0 ^ 0 = 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
⊢ IsBigOWith (c ^ r) l (fun x ↦ f x ^ r) fun x ↦ g x ^ r

Tactic:
apply IsBigOWith.of_bound

Goal state after:
α : Type u_1
r c : ℝ
l : Filter α
f g : α → ℝ
h : IsBigOWith c l f g
hc : 0 ≤ c
hr : 0 ≤ r
hg : 0 ≤ᶠ[l] g
⊢ ∀ᶠ (x : α) in l, ‖f x ^ r‖ ≤ c ^ r * ‖g x ^ r‖
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: z : ℂ
hz : z ≠ 0
w : ℂ
⊢ ‖z ^ w‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
rw [cpow_def_of_ne_zero hz, norm_exp, mul_re, log_re, log_im, Real.exp_sub,
    Real.rpow_def_of_pos (norm_pos_iff.mpr hz)]

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

Goal state before:
pp: x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
⊢ (x ^ (↑n)⁻¹) ^ n = x

Tactic:
by
  have hn0 : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hn
  rw [← rpow_natCast, ← rpow_mul hx, inv_mul_cancel₀ hn0, rpow_one]

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

Goal state before:
pp: case refine_1
z : ℂ
hz : 0 < z.re
hz₀ : z ≠ 0
⊢ Tendsto (fun x ↦ ‖x.1‖ ^ x.2.re) (𝓝 (0, z)) (𝓝 0)

Tactic:
convert!
    (continuous_fst.norm.tendsto ((0 : ℂ), z)).rpow ((continuous_re.comp continuous_snd).tendsto _)
      _ <;>
      simp [hz, Real.zero_rpow hz.ne']

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

Goal state before:
pp: case inr.inr
y : ℝ
H : y < 0
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ∞

Tactic:
· simp [H, asymm H, ne_of_lt, zero_rpow_of_neg]

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

Goal state before:
pp: case inl
x y z : ℝ
hy : 0 < y
h : log x ≤ z * log y
hx : x ≤ 0
⊢ x ≤ y ^ z

pp: case inr
x y z : ℝ
hy : 0 < y
h : log x ≤ z * log y
hx : 0 < x
⊢ x ≤ y ^ z

Tactic:
· exact hx.trans (rpow_pos_of_pos hy _).le

Goal state after:
case inr
x y z : ℝ
hy : 0 < y
h : log x ≤ z * log y
hx : 0 < x
⊢ x ≤ y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ z⁻¹ ≤ y ^ (z * z⁻¹) ↔ x ≤ y ^ z

Tactic:
ENNReal.rpow_mul,

Goal state after:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ z⁻¹ ≤ (y ^ z) ^ z⁻¹ ↔ x ≤ y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
z : ℝ
hx : 1 < x
hz : z < 0
⊢ x ^ z < 1

Tactic:
cases x
  · simp [top_rpow_of_neg hz, zero_lt_one]
  · simp only [one_lt_coe_iff] at hx
    simp [← coe_rpow_of_ne_zero (ne_of_gt (lt_trans zero_lt_one hx)),
      NNReal.rpow_lt_one_of_one_lt_of_neg hx hz]

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

Goal state before:
pp: z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < ↑x
hx2 : ↑x ≤ 1
⊢ 1 ≤ ↑x ^ z

Tactic:
simp only [coe_le_one_iff, coe_pos] at hx1 hx2 ⊢

Goal state after:
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < x
hx2 : x ≤ 1
⊢ 1 ≤ ↑x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: b : ℝ
n : ℕ
h : IsNat b n
a : ℝ≥0
⊢ a ^ b = a ^ n

Tactic:
rw [h.1, NNReal.rpow_natCast]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
hxy : SameRay R x y
hx : x ≠ 0
hyz : SameRay R y 0
hy : y = 0 → x = 0 ∨ 0 = 0
⊢ SameRay R x 0

pp: case inr.inr
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
⊢ SameRay R x z

Tactic:
· exact zero_right x

Goal state after:
case inr.inr
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
⊢ SameRay R x z
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
x y : M
f : M →ₗ[R] N
h✝ : SameRay R x y
x✝ : ∃ r₁ r₂, 0 < r₁ ∧ 0 < r₂ ∧ r₁ • x = r₂ • y
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • y
⊢ r₁ • f x = r₂ • f y

Tactic:
by rw [← f.map_smul, ← f.map_smul, h]

Goal state after:
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: case a
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x : E
s : Set E
h : StarConvex 𝕜 x s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ a / (a + b) + b / (a + b) = 1

Tactic:
· rw [← add_div]
      exact div_self hab.ne'

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
S : AffineSpace V P
contra : ↑⊥ = ↑⊤
⊢ False

Tactic:
bot_coe,

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
S : AffineSpace V P
contra : ∅ = ↑⊤
⊢ False
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
S : AffineSpace V P
⊢ vectorSpan k ↑⊥ = ⊥

Tactic:
bot_coe,

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
S : AffineSpace V P
⊢ vectorSpan k ∅ = ⊥
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
S : AffineSpace V P
Q : AffineSubspace k P
⊢ Q = ⊥ ∨ Q ≠ ⊥

Tactic:
apply eq_or_ne

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

Goal state before:
pp: 𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁸ : NormedDivisionRing 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
s : Set E
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : Module 𝕜 𝕝
inst✝³ : NormSMulClass 𝕜 𝕝
inst✝² : SMulWithZero 𝕝 E
inst✝¹ : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst✝ : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
⊢ b • x ∈ s

Tactic:
by
  rcases eq_or_ne a 0 with rfl | ha₀
  · simp_all
  · calc
      (a⁻¹ • b) • a • x ∈ s := by
        refine hs.smul_mem ?_ ha
        rw [norm_smul, norm_inv, ← div_eq_inv_mul]
        exact div_le_one_of_le₀ hba (norm_nonneg _)
      (a⁻¹ • b) • a • x = b • x := by rw [smul_comm, smul_assoc, smul_inv_smul₀ ha₀]

Goal state after: