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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
mβ : MeasurableSpace β
inst✝¹ : TopologicalSpace β
μ : Measure β
inst✝ : μ.OuterRegular
f : α → β
f_cont : Continuous[inst✝², inst✝¹] f
f_me : MeasurableEmbedding f
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > μ (f '' A)
U : Set β
hUA : U ⊇ f '' A
Uopen : IsOpen[inst✝¹] U
hμU : μ U < r
⊢ (comap f μ) (f ⁻¹' U) < r

Tactic:
rw [f_me.comap_apply]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
mβ : MeasurableSpace β
inst✝¹ : TopologicalSpace β
μ : Measure β
inst✝ : μ.OuterRegular
f : α → β
f_cont : Continuous[inst✝², inst✝¹] f
f_me : MeasurableEmbedding f
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > μ (f '' A)
U : Set β
hUA : U ⊇ f '' A
Uopen : IsOpen[inst✝¹] U
hμU : μ U < r
⊢ μ (f '' f ⁻¹' U) < r
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
h : ↥H
g : G
⊢ RightCosetEquivalence (↑H) (↑h * g) g

Tactic:
simp [RightCosetEquivalence, ← smul_smul]

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

Goal state before:
pp: G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h ↦ g * h) ⁻¹' A) = μ A) ↔ μ.IsMulLeftInvariant

Tactic:
trans ∀ g, map (g * ·) μ = μ

Goal state after:
G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h ↦ g * h) ⁻¹' A) = μ A) ↔
    ∀ (g : G), Measure.map (fun x ↦ g * x) μ = μ

G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G), Measure.map (fun x ↦ g * x) μ = μ) ↔ μ.IsMulLeftInvariant
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSpace H
inst✝³ : DivisionMonoid G
inst✝² : MeasurableMul G
inst✝¹ : MeasurableInv G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
g : G
| μ.inv

Tactic:
← map_mul_right_eq_self μ g⁻¹

Goal state after:
G : Type u_1
H : Type u_2
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSpace H
inst✝³ : DivisionMonoid G
inst✝² : MeasurableMul G
inst✝¹ : MeasurableInv G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
g : G
| (map (fun x ↦ x * g⁻¹) μ).inv
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 : G
⊢ ∫⁻ (y : G), ∫⁻ (x_1 : G), f y * (g (y⁻¹ * x_1) * k ((y⁻¹ * x_1)⁻¹ * (y⁻¹ * x))) ∂μ ∂μ =
    ∫⁻ (y : G), ∫⁻ (a : G), f a * g (a⁻¹ * y) * k (y⁻¹ * x) ∂μ ∂μ

Tactic:
lintegral_lintegral_swap

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 : G
⊢ ∫⁻ (y : G), ∫⁻ (x_1 : G), f x_1 * (g (x_1⁻¹ * y) * k ((x_1⁻¹ * y)⁻¹ * (x_1⁻¹ * x))) ∂μ ∂μ =
    ∫⁻ (y : G), ∫⁻ (a : G), f a * g (a⁻¹ * y) * k (y⁻¹ * x) ∂μ ∂μ

case hf
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 : G
⊢ AEMeasurable (Function.uncurry fun y x_1 ↦ f y * (g (y⁻¹ * x_1) * k ((y⁻¹ * x_1)⁻¹ * (y⁻¹ * x)))) (μ.prod μ)
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case a
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
K : Set α
hK : IsCompact K
⊢ ⨅ U, ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen[inst✝⁴] U), μ U ≤ μ K

Tactic:
· apply le_of_forall_gt
    simpa only [iInf_lt_iff, exists_prop, exists_and_left] using hK.exists_isOpen_lt_of_lt

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∞
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f ≤ ∫⁻ (a : α), (f * g) a ∂μ

Tactic:
by
  rw [← iSup_lintegral_measurable_le_eq_lintegral, ← iSup_lintegral_measurable_le_eq_lintegral]
  refine iSup₂_le fun i i_meas => iSup_le fun hi => ?_
  rw [lintegral_withDensity_eq_lintegral_mul _ f_meas i_meas]
  exact le_iSup₂_of_le (f * i) (f_meas.mul i_meas) <| le_iSup_of_le (by grw [hi]) le_rfl

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

Goal state before:
pp: x : ℝ
h : -1 ≤ x
⊢ √(1 + x) ≤ 1 + x / 2

Tactic:
refine sqrt_le_iff.mpr ⟨by linarith, ?_⟩
  calc 1 + x
    _ ≤ 1 + x + (x / 2) ^ 2 := le_add_of_nonneg_right <| sq_nonneg _
    _ = _ := by ring

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ((μ.withDensity f).withDensity fun x ↦ (f x)⁻¹) ≤ μ

Tactic:
← withDensity_mul₀ hf hf.fun_inv

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ μ.withDensity (f * fun i ↦ (f i)⁻¹) ≤ μ
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
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ ((μ.withDensity f).withDensity fun x ↦ (f x)⁻¹) = μ

Tactic:
← withDensity_mul₀ hf hf.fun_inv

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ μ.withDensity (f * fun i ↦ (f i)⁻¹) = μ
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_7
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
hc : IsUnit c
f : α → β
⊢ HasFiniteIntegral (c • f) μ ↔ HasFiniteIntegral f μ

Tactic:
obtain ⟨c, rfl⟩ := hc
  constructor
  · intro h
    simpa only [smul_smul, Units.inv_mul, one_smul] using h.smul ((c⁻¹ : 𝕜ˣ) : 𝕜)
  exact HasFiniteIntegral.smul _

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

Goal state before:
pp: a b : ℂ
⊢ { re := (a * b).re, im := -(a * b).im } = { re := b.re, im := -b.im } * { re := a.re, im := -a.im }

Tactic:
ext <;> simp [add_comm]

Goal state after:
case a
a b : ℂ
⊢ a.re * b.re - a.im * b.im = b.re * a.re - b.im * a.im

case a
a b : ℂ
⊢ -(a.re * b.im) + -(a.im * b.re) = -(b.re * a.im) + -(b.im * a.re)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: a b : ℂ
⊢ { re := (a + b).re, im := -(a + b).im } = { re := a.re, im := -a.im } + { re := b.re, im := -b.im }

Tactic:
ext <;> simp [add_comm]

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

Goal state before:
pp: z : ℂ
x : ℝ
⊢ z / ↑x = { re := z.re / x, im := z.im / x }

Tactic:
simp_rw [div_eq_inv_mul, ← ofReal_inv, ofReal_mul']

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

Goal state before:
pp: A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
x y : A
h₁ : ℜ x = ℜ y
h₂ : ℑ x = ℑ y
⊢ x = y

Tactic:
← realPart_add_I_smul_imaginaryPart x,

Goal state after:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
x y : A
h₁ : ℜ x = ℜ y
h₂ : ℑ x = ℑ y
⊢ ↑(ℜ x) + I • ↑(ℑ x) = y
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
x : K
⊢ ‖imLm x‖ ≤ 1 * ‖x‖

Tactic:
rw [one_mul]
    exact abs_im_le_norm x

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ I = 0 ∨ I * I = -1

Tactic:
exact h.I_mul_I_ax

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

Goal state before:
pp: n x : ℕ
h₁ : IsNat n x
a : ℕ
h₂ : ascFactorial 1 x = a
⊢ IsNat n ! a

Tactic:
by
  constructor
  simp only [h₁.out, cast_id, ← h₂, one_ascFactorial]

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

Goal state before:
pp: α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (f =o[l] fun x ↦ c • f' x) ↔ f =o[l] f'

Tactic:
← isLittleO_norm_right

Goal state after:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (f =o[l] fun x ↦ ‖c • f' x‖) ↔ f =o[l] f'
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case mp
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ u =o[l] v → ∃ φ, Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v

pp: case mpr
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ (∃ φ, Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v) → u =o[l] v

Tactic:
· exact fun h => ⟨fun x => u x / v x, h.tendsto_div_nhds_zero, h.eventually_mul_div_cancel.symm⟩

Goal state after:
case mpr
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ (∃ φ, Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v) → u =o[l] v
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : x ∈ {x | (fun x ↦ ‖f₁ x‖ ≤ c * ‖f₂ x‖) x}
⊢ x ∈ {x | (fun x ↦ ‖f₂ x‖ ≤ 1 / (1 - c) * ‖f₂ x - f₁ x‖) x}

Tactic:
simp only [mem_ofPred_eq] at hx ⊢

Goal state after:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖
⊢ ‖f₂ x‖ ≤ 1 / (1 - c) * ‖f₂ x - f₁ x‖
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ IsBigOWith c l (fun x ↦ f x * g x) h ↔ IsBigOWith c l g fun x ↦ h x / f x

Tactic:
isBigOWith_iff,

Goal state after:
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h x‖) ↔ IsBigOWith c l g fun x ↦ h x / f x
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑(tan x) = ↑(sin x / cos x)

Tactic:
by simp only [ofReal_tan, tan_eq_sin_div_cos, ofReal_div, ofReal_sin,
    ofReal_cos]

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

Goal state before:
pp: x : ℝ
⊢ ((cexp ↑x + cexp (-↑x)) / 2 * 2).re = (cexp ↑x).re + (cexp (-↑x)).re

Tactic:
div_mul_cancel₀ _ (two_ne_zero' ℂ),

Goal state after:
x : ℝ
⊢ (cexp ↑x + cexp (-↑x)).re = (cexp ↑x).re + (cexp (-↑x)).re
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find h).pred • ε
j : ℕ
hj : j ≥ i
hfij : f j ≤ f i
| a - l.pred • ε = a - l • ε + ε

Tactic:
conv =>

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find h).pred • ε
j : ℕ
hj : j ≥ i
hfij : f j ≤ f i
| a - l.pred • ε
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
m : ℕ
| (1 - abv x ^ m) / -(abv x - 1)

Tactic:
neg_sub

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
m : ℕ
| (1 - abv x ^ m) / (1 - abv x)
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: x : ℝ
⊢ rexp (x / 2) = √(rexp x)

Tactic:
by
  rw [eq_comm, sqrt_eq_iff_eq_sq, sq, ← exp_add, add_halves] <;> exact (exp_pos _).le

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) →
      ∀ (m : ℕ), n.succ ≤ m → m = k + n.succ → abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
kn : k + n.succ ≥ n.succ
⊢ abv (f (k + n.succ).succ) ≤ ?m.259 * r

Tactic:
rw [mul_comm] <;> exact h _ (Nat.le_of_succ_le kn)

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

Goal state before:
pp: ⊢ cos (2 * (π / 2)) = -1

Tactic:
cos_two_mul,

Goal state after:
⊢ 2 * cos (π / 2) ^ 2 - 1 = -1
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NontrivialTopology E
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : ‖y‖ = r
⊢ x + y ∈ sphere x r

Tactic:
simpa using hy

Goal state after:
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
s : Set 𝕜
hs : 0 ∉ s
r : ℝ
⊢ ⋃ c ∈ s, sphere 0 (‖c‖ * r) = (fun x ↦ ‖x‖) ⁻¹' (fun x ↦ ‖x‖ * r) '' s

Tactic:
by ext; simp [eq_comm]

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

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

Tactic:
← sq_cos_pi_div_six

Goal state after:
⊢ cos (π / 2 - π / 3) ^ 2 = cos (π / 6) ^ 2
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:

Tactic:
fun n ↦ ‖↑(u n) * r ^ n‖
  _ =O[atTop] fun n ↦ u n * ‖r‖ ^ n := by
      apply (IsBigOWith.of_bound (c := ‖(1 : R)‖) ?_).isBigO
      filter_upwards [eventually_norm_pow_le r] with n hn
      simp only [norm_mul, Real.norm_eq_abs, abs_cast, norm_pow, abs_norm]
      apply (norm_mul_le _ _).trans
      have : ‖(u n : R)‖ * ‖r ^ n‖ ≤ (u n * ‖(1 : R)‖) * ‖r‖ ^ n := by
        gcongr; exact norm_cast_le (u n)
      exact this.trans (le_of_eq (by ring))
  _ =O[atTop] fun n ↦ ↑(n ^ k) * ‖r‖ ^ n := hu.mul (isBigO_refl _ _)
  _ =O[atTop] fun n ↦ r' ^ n := by
      simp only [cast_pow]
      exact (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt k hrr').isBigO

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

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
h : CauchySeq fun n ↦ ∑ k ∈ Finset.range n, f k
b : ℕ → ℝ
left✝ : ∀ (n : ℕ), 0 ≤ b n
key : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (∑ k ∈ Finset.range n, f k) (∑ k ∈ Finset.range m, f k) ≤ b N
right✝ : Tendsto b atTop (𝓝 0)
⊢ ∃ C, ∀ (n : ℕ), ‖f n‖ ≤ C

Tactic:
refine ⟨b 0, fun n ↦ ?_⟩

Goal state after:
α : Type u_1
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
h : CauchySeq fun n ↦ ∑ k ∈ Finset.range n, f k
b : ℕ → ℝ
left✝ : ∀ (n : ℕ), 0 ≤ b n
key : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (∑ k ∈ Finset.range n, f k) (∑ k ∈ Finset.range m, f k) ≤ b N
right✝ : Tendsto b atTop (𝓝 0)
n : ℕ
⊢ ‖f n‖ ≤ b 0
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
⊢ IsPathConnected F ↔ ∃ x ∈ F, pathComponentIn F x = F

Tactic:
constructor <;> rintro ⟨x, x_in, h⟩ <;> use x, x_in

Goal state after:
case right
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
⊢ pathComponentIn F x = F

case right
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn F x = F
⊢ ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
⊢ (ofLine ⋯ ⋯ ⋯) t = γ t

Tactic:
simp [ofLine]

Goal state after:
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 : ℝ
ht : 1 / 2 ≤ t
| (γ₁.trans γ₂).extend t

Tactic:
← sub_sub_cancel 1 t

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
| (γ₁.trans γ₂).extend (1 - (1 - t))
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n : ℕ
| ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C

Tactic:
conv =>

Goal state after:
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n✝ n : ℕ
| ‖f n‖ ≤ C / ‖w‖ ^ n
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p x : ℝ
⊢ ‖↑x‖ = ‖↑x‖

Tactic:
suffices ‖(↑(-1 * x) : AddCircle (-1 * p))‖ = ‖(x : AddCircle p)‖ by
    rw [← this, neg_one_mul]
    simp
  simp only [norm_coe_mul, abs_neg, abs_one, one_mul]

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

Goal state before:
pp: case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
hx : ‖↑(p⁻¹ * x)‖ = |p⁻¹| * ‖↑x‖
⊢ ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|

Tactic:
rw [abs_inv, eq_inv_mul_iff_mul_eq₀ ((not_congr abs_eq_zero).mpr hp)] at hx

Goal state after:
case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
hx : |p| * ‖↑(p⁻¹ * x)‖ = ‖↑x‖
⊢ ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case refine_1
x r : ℝ
hr : r ≤ ‖↑x‖
⊢ r ≤ |x - ↑(round x)|

Tactic:
abs_sub_round_eq_min,

Goal state after:
case refine_1
x r : ℝ
hr : r ≤ ‖↑x‖
⊢ r ≤ min (fract x) (1 - fract x)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n + 1 + 1 + 1), (-1) ^ i * f i

Tactic:
sum_range_succ _ (2 * n + 1 + 1),

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i ≤
    ∑ x ∈ Finset.range (2 * n + 1 + 1), (-1) ^ x * f x + (-1) ^ (2 * n + 1 + 1) * f (2 * n + 1 + 1)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
⊢ Real.sin x.arg = x.im / ‖x‖

Tactic:
unfold arg; split_ifs <;>
    simp [sub_eq_add_neg, Real.sin_arcsin (abs_le.1 (abs_im_div_norm_le_one x)).1
      (abs_le.1 (abs_im_div_norm_le_one x)).2, Real.sin_add, neg_div, Real.arcsin_neg, Real.sin_neg]

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

Goal state before:
pp: case mp
x : ℝ
⊢ log x = 0 → x = 0 ∨ x = 1 ∨ x = -1

Tactic:
intro h
    rcases lt_trichotomy x 0 with (x_lt_zero | rfl | x_gt_zero)
    · refine Or.inr (Or.inr (neg_eq_iff_eq_neg.mp ?_))
      rw [← log_neg_eq_log x] at h
      exact eq_one_of_pos_of_log_eq_zero (neg_pos.mpr x_lt_zero) h
    · exact Or.inl rfl
    · exact Or.inr (Or.inl (eq_one_of_pos_of_log_eq_zero x_gt_zero h))

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

Goal state before:
pp: case succ.inr
x : ℝ
n : ℕ
ih : log (x ^ n) = ↑n * log x
hx : x ≠ 0
⊢ log (x ^ n) + log x = ↑(n + 1) * log x

Tactic:
ih,

Goal state after:
case succ.inr
x : ℝ
n : ℕ
ih : log (x ^ n) = ↑n * log x
hx : x ≠ 0
⊢ ↑n * log x + log x = ↑(n + 1) * log x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

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

Tactic:
simp only [cpow_def, neg_eq_zero, mul_neg]

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

Goal state before:
pp: case mp
θ ψ : ℝ
⊢ sin θ = sin ψ → ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π

pp: case mpr
θ ψ : ℝ
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π → sin θ = sin ψ

Tactic:
· intro Hsin
    rw [← cos_pi_div_two_sub, ← cos_pi_div_two_sub] at Hsin
    rcases cos_eq_iff_coe_eq_or_eq_neg.mp Hsin with h | h
    · left
      rw [coe_sub, coe_sub] at h
      exact sub_right_inj.1 h
    right
    rw [coe_sub, coe_sub, eq_neg_iff_add_eq_zero, add_sub, sub_add_eq_add_sub, ← coe_add,
      add_halves, sub_sub, sub_eq_zero] at h
    exact h.symm

Goal state after:
case mpr
θ ψ : ℝ
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π → sin θ = sin ψ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ -z.im < ‖z‖

pp: case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ 0 < ‖z‖

Tactic:
← abs_of_neg him,

Goal state after:
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ |z.im| < ‖z‖

case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ 0 < ‖z‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

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

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

Goal state before:
pp: θ : ℝ
⊢ |(-↑θ).toReal| = θ ↔ 0 ≤ θ ∧ θ ≤ π

Tactic:
refine ⟨fun h => h ▸ ⟨abs_nonneg _, abs_toReal_le_pi _⟩, fun h => ?_⟩
  by_cases hnegpi : θ = π; · simp [hnegpi, Real.pi_pos.le]
  rw [← coe_neg,
    toReal_coe_eq_self_iff.2
      ⟨neg_lt_neg (lt_of_le_of_ne h.2 hnegpi), (neg_nonpos.2 h.1).trans Real.pi_pos.le⟩,
    abs_neg, abs_eq_self.2 h.1]

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

Goal state before:
pp: case inr.inl.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re < 0
⊢ ↑0 = ↑(2 * π)

Tactic:
Real.Angle.coe_two_pi,

Goal state after:
case inr.inl.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re < 0
⊢ ↑0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.succ
x : ℂ
x0 : x ≠ 0
n : ℕ
ih : ↑(x ^ n).arg = n • ↑x.arg
⊢ ↑(x ^ n).arg + ↑x.arg = (n + 1) • ↑x.arg

Tactic:
ih,

Goal state after:
case inr.succ
x : ℂ
x0 : x ≠ 0
n : ℕ
ih : ↑(x ^ n).arg = n • ↑x.arg
⊢ n • ↑x.arg + ↑x.arg = (n + 1) • ↑x.arg
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case pos
x a : ℝ
hyp : (0 ^ ↑x).re = a
h : x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
subst h
      simp only [Complex.one_re, Complex.ofReal_zero, Complex.cpow_zero] at hyp
      exact Or.inr ⟨rfl, hyp.symm⟩

Goal state after: