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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h : μ.InnerRegularWRT p fun s ↦ MeasurableSet s ∧ μ s ≠ ∞
A s : Set α
s_meas : MeasurableSet s
hs : μ (s ∩ A) ≠ ∞
r : ℝ≥0∞
hr : r < (μ.restrict A) s
⊢ (μ.restrict A) s ≤ μ (toMeasurable μ (s ∩ A) ∩ s)

Tactic:
rw [restrict_apply s_meas]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : Set α → Prop
h : μ.InnerRegularWRT p fun s ↦ MeasurableSet s ∧ μ s ≠ ∞
A s : Set α
s_meas : MeasurableSet s
hs : μ (s ∩ A) ≠ ∞
r : ℝ≥0∞
hr : r < (μ.restrict A) s
⊢ μ (s ∩ A) ≤ μ (toMeasurable μ (s ∩ A) ∩ s)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
t : Set β
i : ℕ × ℕ
s' : Set α
t' : Set β
hs' : MeasurableSet s'
ht' : MeasurableSet t'
⊢ (((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)).restrict (s ×ˢ t)) (s' ×ˢ t') =
    ((sfiniteSeq μ i.1).restrict s) s' * ((sfiniteSeq ν i.2).restrict t) t'

Tactic:
rw [restrict_apply (hs'.prod ht'), prod_inter_prod, prod_prod, restrict_apply hs',
    restrict_apply ht']

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
hA : MeasurableSet A
⊢ μ ((fun h ↦ h * g) ⁻¹' A) = μ A ↔ (Measure.map (fun x ↦ x * g) μ) A = μ A

Tactic:
map_apply (measurable_mul_const g) hA

Goal state after:
G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
g : G
A : Set G
hA : MeasurableSet A
⊢ μ ((fun h ↦ h * g) ⁻¹' A) = μ A ↔ μ ((fun x ↦ x * g) ⁻¹' A) = μ A
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: X : Type u_6
E : Type u_7
ι : Type u_8
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : CommMonoid E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : IsCompletelyPseudoMetrizableSpace E
inst✝⁶ : SecondCountableTopology E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableMul₂ E
inst✝² : Countable ι
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable (fun x ↦ ∏'[L] (i : ι), f i x) μ

Tactic:
choose g hg_meas hg_eq_f using h

Goal state after:
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝¹⁰ : MeasurableSpace X
inst✝⁹ : CommMonoid E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : IsCompletelyPseudoMetrizableSpace E
inst✝⁶ : SecondCountableTopology E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableMul₂ E
inst✝² : Countable ι
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f g : ι → X → E
hg_meas : ∀ (i : ι), Measurable (g i)
hg_eq_f : ∀ (i : ι), f i =ᵐ[μ] g i
⊢ AEMeasurable (fun x ↦ ∏'[L] (i : ι), f i x) μ
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
⊢ ρ.snd univ = ρ univ

Tactic:
snd_apply MeasurableSet.univ,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
⊢ ρ (Prod.snd ⁻¹' univ) = ρ univ
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case neg
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝¹ : ¬(L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite)
h✝ : ¬HasProd (fun i ↦ f i) 1 L
⊢ AEMeasurable (Exists.choose hm) μ

Tactic:
apply aemeasurable_of_tendsto_metrizable_ae L.filter (f := fun s => ∏ i ∈ s, f i)

Goal state after:
case neg.hf
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝¹ : ¬(L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite)
h✝ : ¬HasProd (fun i ↦ f i) 1 L
⊢ ∀ (n : Finset ι), AEMeasurable (∏ i ∈ n, f i) μ

case neg.h_tendsto
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝¹ : ¬(L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite)
h✝ : ¬HasProd (fun i ↦ f i) 1 L
⊢ ∀ᵐ (x : X) ∂μ, Tendsto (fun n ↦ (∏ i ∈ n, f i) x) L.filter (𝓝 (Exists.choose hm x))
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : ContinuousMul G
inst✝ : BorelSpace G
g : G
⊢ μ {g} = μ {1}

Tactic:
convert! measure_preimage_mul μ g⁻¹ _

Goal state after:
case e'_2
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : ContinuousMul G
inst✝ : BorelSpace G
g : G
⊢ {g} = (fun h ↦ g⁻¹ * h) ⁻¹' {1}
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
μ✝ : Measure G
inst✝⁶ : μ✝.IsHaarMeasure
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
inst✝³ : T1Space G
inst✝² : WeaklyLocallyCompactSpace G
inst✝¹ : (𝓝[≠] 1).NeBot
μ : Measure G
inst✝ : μ.IsHaarMeasure
x✝ : μ 1 = 0 ∨ μ 1 ≠ 0
⊢ NullSingletonClass μ

Tactic:
cases eq_or_ne (μ 1) 0 with

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
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
sm : MeasurableSet s
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
f : G → ℝ≥0∞
hf : Measurable f
g : G → ℝ≥0∞ := fun y ↦ f y⁻¹ / ν' ((fun x ↦ x * y⁻¹) ⁻¹' s)
hg : Measurable g
x : G
hx : ν' ((fun y ↦ y * x) ⁻¹' s) < ∞
⊢ (fun x ↦ ν' ((fun z ↦ z * x) ⁻¹' s) * (f x / ν' ((fun z ↦ z * x) ⁻¹' s))) x = f x

Tactic:
simp_rw [ENNReal.mul_div_cancel (measure_mul_right_ne_zero ν' h2s _) hx.ne]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
a : α
s : Set α
hs : MeasurableSet s
⊢ ((dirac a).withDensity f) s = (f a • dirac a) s

Tactic:
simp [withDensity_apply f hs, setLIntegral_dirac, Set.indicator]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x ↦ (f x)⁻¹ * i x) ≤ g
⊢ ∀ (a : α), f a < ∞ → i a ≤ (f * fun i_1 ↦ (f i_1)⁻¹ * i i_1) a

Tactic:
intro x h'x

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
⊢ i x ≤ (f * fun i_1 ↦ (f i_1)⁻¹ * i i_1) x
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
⊢ i x ≤ (f * fun i_1 ↦ (f i_1)⁻¹ * i i_1) x

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

Goal state after:
case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
hx : f x = 0
⊢ i x ≤ (f * fun i_1 ↦ (f i_1)⁻¹ * i i_1) x

case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
hx : f x ≠ 0
⊢ i x ≤ (f * fun i_1 ↦ (f i_1)⁻¹ * i i_1) x
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: case h₁
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ x ^ 2 ≤ m ^ 2

Tactic:
rw [sq_le_sq, abs_of_nonneg hm₀]

Goal state after:
case h₁
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ |x| ≤ m
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: case h₂
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ y ^ 2 ≤ m ^ 2

Tactic:
rw [sq_le_sq, abs_of_nonneg hm₀]

Goal state after:
case h₂
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ |y| ≤ m
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:

Tactic:
∫⁻ a, b a ∂μ = 2 * ∫⁻ a, ENNReal.ofReal (bound a) ∂μ := by
          rw [lintegral_const_mul']
          finiteness
        _ ≠ ∞ := mul_ne_top coe_ne_top bound_hasFiniteIntegral.ne

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst✝ : PosSMulMono ℚ≥0 α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, f x ≤ a
⊢ ∑ i ∈ s, (fun i ↦ f i) i ≤ ↑(#s) • a

Tactic:
by
    rw [Nat.cast_smul_eq_nsmul]; exact sum_le_card_nsmul _ _ _ h

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

Goal state before:
pp: G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
x : G
⊢ ∫⁻ (y : G), ((fun z ↦ f z.1 * g z.2) * fun z ↦ φ (z.1 * z.2)) (x, y) ∂μ = ?m.96 x

Tactic:
by apply (lintegral_mul_left_eq_self _ x⁻¹).symm

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ star (U * B) * (U * B) = star B * star U * U * B

Tactic:
simp only [mul_assoc, star_mul]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Ring 𝕜₂
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : 𝕜 →ₗ[𝕜] E
x : 𝕜
⊢ ‖f x‖ ≤ ‖f 1‖ * ‖x‖

Tactic:
conv_lhs => rw [← mul_one x]

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Ring 𝕜₂
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : 𝕜 →ₗ[𝕜] E
x : 𝕜
⊢ ‖f (x * 1)‖ ≤ ‖f 1‖ * ‖x‖
Module: Mathlib.LinearAlgebra.Complex.Module

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

Tactic:
simp [smul_re, smul_im, smul_zero]

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
⊢ (r • 0).im = im 0

Tactic:
simp [smul_re, smul_im, smul_zero]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
r : R
x✝ : ℂ
xr xi : ℝ
⊢ (ofRealHom.comp (algebraMap R ℝ)) r * { re := xr, im := xi } =
    { re := xr, im := xi } * (ofRealHom.comp (algebraMap R ℝ)) r

Tactic:
ext <;> simp [Algebra.commutes]

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

Goal state before:
pp: z : ℂ
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℂ
⊢ ‖imLm x‖ ≤ 1 * ‖x‖

Tactic:
by simp [abs_im_le_norm]

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
a : A
a_eq : a = ↑(ℜ a) + I • ↑(ℑ a)
⊢ ↑(ℜ a) * ↑(ℜ a) + -(I • (↑(ℑ a) * ↑(ℜ a))) + (I • (↑(ℜ a) * ↑(ℑ a)) + ↑(ℑ a) * ↑(ℑ a)) +
      (↑(ℜ a) * ↑(ℜ a) + I • (↑(ℑ a) * ↑(ℜ a)) + (↑(ℑ a) * ↑(ℑ a) + -(I • (↑(ℜ a) * ↑(ℑ a))))) =
    2 • (↑(ℜ a) * ↑(ℜ a)) + 2 • (↑(ℑ a) * ↑(ℑ a))

Tactic:
abel

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ z⁻¹ = (starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹

Tactic:
rcases eq_or_ne z 0 with (rfl | h₀)
  · simp
  · apply inv_eq_of_mul_eq_one_right
    rw [← mul_assoc, mul_conj, ofReal_inv, ofReal_pow, mul_inv_cancel₀]
    simpa

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

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : PartialHomeomorph X Y
h : e.source = univ
h' : e.target = univ
x : X
⊢ x ∈ e.source

Tactic:
by
      rw [h]
      exact mem_univ _

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Z → X
x : Z
h : f ⁻¹' e.source ∈ 𝓝 x
⊢ ContinuousAt f x ↔ ContinuousAt (↑e ∘ f) x

Tactic:
by
  have hx : f x ∈ e.source := (mem_of_mem_nhds h :)
  have h' : f ⁻¹' e.source ∈ 𝓝[univ] x := by rwa [nhdsWithin_univ]
  rw [← continuousWithinAt_univ, ← continuousWithinAt_univ,
    e.continuousWithinAt_iff_continuousWithinAt_comp_left hx h']

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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (r : ℝ),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          im)
        ({ toFun := ⇑(algebraMap ℝ 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r) =
      0

Tactic:
by subst h''; exact h.ofReal_im_ax

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
l : Filter α
hc : 0 < c
⊢ IsBigOWith c⁻¹ l f g ↔ ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖

Tactic:
by
  simp only [IsBigOWith_def, ← div_eq_inv_mul, le_div_iff₀' hc]

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c₁ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖ ↔ ‖f₂ x‖ ≤ c₁ * ‖g₂ x‖

Tactic:
filter_upwards [hf, hg] with _ e₁ e₂

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c₁ : ℝ
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
a✝ : α
e₁ : f₁ a✝ = f₂ a✝
e₂ : g₁ a✝ = g₂ a✝
⊢ ‖f₁ a✝‖ ≤ c₁ * ‖g₁ a✝‖ ↔ ‖f₂ a✝‖ ≤ c₁ * ‖g₂ a✝‖
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
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
⊢ ∃ i,
    ∀ j ≥ i, abv ((∑ k ∈ range j, f k) * ∑ k ∈ range j, g k - ∑ n ∈ range j, ∑ m ∈ range (n + 1), f m * g (n - m)) < ε

Tactic:
have hP0 : 0 < P := lt_of_le_of_lt (abs_nonneg _) (hP 0)

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
⊢ ∃ i,
    ∀ j ≥ i, abv ((∑ k ∈ range j, f k) * ∑ k ∈ range j, g k - ∑ n ∈ range j, ∑ m ∈ range (n + 1), f m * g (n - m)) < ε
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 α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
h : ∀ i ∈ s, IsBigOWith (C i) l (A i) g
⊢ IsBigOWith (∑ i ∈ s, C i) l (∑ i ∈ s, A i) g

Tactic:
by
  induction s using Finset.cons_induction with
  | empty =>
      rw [Finset.sum_empty]
      apply isBigOWith_zero'
  | cons i s is IH =>
    simp only [Finset.sum_cons, Finset.forall_mem_cons] at h ⊢
    exact h.1.add (IH h.2)

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
⊢ (f =o[l] fun x ↦ c • f' x) ↔ f =o[l] f'

Tactic:
have cne0 : ‖c‖ ≠ 0 := norm_ne_zero_iff.mpr hc
  rw [← isLittleO_norm_right]
  simp only [norm_smul]
  rw [isLittleO_const_mul_right_iff cne0, isLittleO_norm_right]

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

Goal state before:
pp: x y : ℂ
⊢ sinh (x + y) = sinh x * cosh y + cosh x * sinh y

Tactic:
rw [← mul_right_inj' (two_ne_zero' ℂ), two_sinh, exp_add, neg_add, exp_add, eq_comm, mul_add, ←
    mul_assoc, two_sinh, mul_left_comm, two_sinh, ← mul_right_inj' (two_ne_zero' ℂ), mul_add,
    mul_left_comm, two_cosh, ← mul_assoc, two_cosh]
  exact sinh_add_aux

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

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

Tactic:
← mul_right_inj' (exp_ne_zero x),

Goal state after:
x : ℂ
⊢ cexp x * cexp (-x) = cexp x * (cexp x)⁻¹
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
hx : 0 < cos x
⊢ tan x / √(1 + tan x ^ 2) = tan x * cos x

Tactic:
← inv_sqrt_one_add_tan_sq hx,

Goal state after:
x : ℝ
hx : 0 < cos x
⊢ tan x / √(1 + tan x ^ 2) = tan x * (√(1 + tan x ^ 2))⁻¹
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : |x| = x
⊢ |x| ≤ 1

Tactic:
rwa [h3]

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

Goal state before:
pp: case inr
x : ℝ
hx : x ≠ 0
⊢ x + 1 ≤ rexp x

Tactic:
· exact (add_one_lt_exp hx).le

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

Goal state before:
pp: r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
⊢ y = x + (y - x)

Tactic:
abel

Goal state after:
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
m_pos : 0 < m
this : abv (f m.pred.succ) ≤ 0 * abv (f m.pred)
⊢ abv (f m) ≤ abv (f n.succ) * 0⁻¹ ^ n.succ * 0 ^ m

Tactic:
simpa [Nat.sub_add_cancel m_pos, pow_succ] using this

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

Goal state before:
pp: n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ rexp ↑⌈x⌉₊ / (rexp 1 * C) ≤ rexp (x + 1) / (rexp 1 * C)

Tactic:
gcongr; exact (Nat.ceil_lt_add_one hx₀.le).le

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

Goal state before:
pp: x : ℝ
⊢ sin x = 0 ↔ cos x * cos x = sin ?m.18 * sin ?m.18 + cos ?m.18 * cos ?m.18

pp: x : ℝ
⊢ ℝ

Tactic:
right_eq_add,

Goal state after:
x : ℝ
⊢ sin x = 0 ↔ sin x * sin x = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

Tactic:
cos_int_mul_two_pi_add_pi

Goal state after:
x : ℝ
n : ℤ
h : -1 = 1
hn : ↑(n / 2) * (2 * π) + π = x
hn1 : n % 2 = 1
⊢ ↑(n / 2) * (2 * π) = x
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ {x} * ball y δ = ball (x * y) δ

Tactic:
by
  simp only [preimage_mul_ball, image_mul_left, singleton_mul, div_inv_eq_mul, mul_comm y x]

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ {y} * ball x δ = ball (x * y) δ

Tactic:
singleton_mul_ball,

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ ball (y * x) δ = ball (x * y) δ
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: case e'_3.f
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ s
x : E
⊢ x ∈ ball x✝¹ δ ↔ x ∈ {x✝¹} * ball 1 δ

Tactic:
singleton_mul_ball,

Goal state after:
case e'_3.f
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ s
x : E
⊢ x ∈ ball x✝¹ δ ↔ x ∈ ball (x✝¹ * 1) δ
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : r < 0
⊢ interior (closedBall x r) = ball x r

pp: case inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : 0 < r
⊢ interior (closedBall x r) = ball x r

Tactic:
· rw [closedBall_eq_empty.2 hr, ball_eq_empty.2 hr.le, interior_empty]

Goal state after:
case inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr✝ : r ≠ 0
hr : 0 < r
⊢ interior (closedBall x r) = ball x r
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 : E
zs : z ∈ s
hz : r • z = -x + y
⊢ ε / R * R = ε

Tactic:
by field

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 z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : dist x z < ε + δ
y : E
yz : dist z y ≤ ε
xy : dist y x < δ
⊢ ∃ y, dist x y < δ ∧ dist y z ≤ ε

Tactic:
exact ⟨y, by simp [dist_comm x y, dist_comm y z, *]⟩

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

Goal state before:
pp: z : ℂ
⊢ sin z = 0 ↔ cos z * cos z = sin ?m.18 * sin ?m.18 + cos ?m.18 * cos ?m.18

pp: z : ℂ
⊢ ℂ

Tactic:
right_eq_add,

Goal state after:
z : ℂ
⊢ sin z = 0 ↔ sin z * sin z = 0