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

Goal state before:
pp: case mpr
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
x✝ : H
⊢ x✝ ∈ (fun x ↦ x * f g) ⁻¹' ⇑f '' s → x✝ ∈ ⇑f '' (fun x ↦ x * g) ⁻¹' s

Tactic:
intro ⟨y, yins, hy⟩
        exact ⟨y * g⁻¹, by simp [yins], by simp [hy]⟩

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

Goal state before:
pp: case zero
G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed[inst✝⁷] K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n ↦ (fun T ↦ T ∪ g T • K)^[n] K
⊢ IsCompact (L 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed[inst✝⁷] K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n ↦ (fun T ↦ T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
⊢ IsClosed[inst✝⁷] (L 0)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed[inst✝⁷] K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n ↦ (fun T ↦ T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
Lclosed : ∀ (n : ℕ), IsClosed[inst✝⁷] (L n)
⊢ μ (L 0) = ↑(0 + 1) * μ K

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ (μ.withDensity f) s

Tactic:
by
  let t := toMeasurable (μ.withDensity f) s
  calc
  ∫⁻ a in s, f a ∂μ ≤ ∫⁻ a in t, f a ∂μ :=
    lintegral_mono_set (subset_toMeasurable (withDensity μ f) s)
  _ = μ.withDensity f t :=
    (withDensity_apply f (measurableSet_toMeasurable (withDensity μ f) s)).symm
  _ = μ.withDensity f s := measure_toMeasurable s

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity (f + g)) s = (μ.withDensity f + μ.withDensity g) s

Tactic:
rw [withDensity_apply _ hs, Measure.add_apply, withDensity_apply _ hs, withDensity_apply _ hs,
    ← lintegral_add_left hf]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (f + g) a ∂μ = ∫⁻ (a : α) in s, f a + g a ∂μ
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
s : Set G
hs : MeasurableSet s
⊢ (map (fun x ↦ x * g) μ) s = 0 → μ s = 0

Tactic:
map_apply (measurable_mul_const g) hs,

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
s : Set G
hs : MeasurableSet s
⊢ μ ((fun x ↦ x * g) ⁻¹' s) = 0 → μ s = 0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
⊢ (μ.withDensity (s.indicator f)) t = ((μ.restrict s).withDensity f) t

Tactic:
withDensity_apply _ ht,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
⊢ ∫⁻ (a : α) in t, s.indicator f a ∂μ = ((μ.restrict s).withDensity f) t
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
⊢ (μ.withDensity f) (t ∩ s) = ((μ.restrict s).withDensity f) t

Tactic:
withDensity_apply _ ht,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
⊢ (μ.withDensity f) (t ∩ s) = ∫⁻ (a : α) in t, f a ∂μ.restrict s
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set α
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
⊢ (μ.withDensity f) (t ∩ s) = ((μ.restrict s).withDensity f) t

Tactic:
withDensity_apply _ ht,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set α
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
⊢ (μ.withDensity f) (t ∩ s) = ∫⁻ (a : α) in t, f a ∂μ.restrict s
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : TopologicalSpace G
inst✝² : BorelSpace G
μ : Measure G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h : μ.InnerRegularCompactLTTop
⊢ μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed[inst✝³] s) fun s ↦ MeasurableSet s ∧ μ s ≠ ∞

Tactic:
intro s ⟨s_meas, μs⟩ r hr

Goal state after:
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : TopologicalSpace G
inst✝² : BorelSpace G
μ : Measure G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h : μ.InnerRegularCompactLTTop
s : Set G
s_meas : MeasurableSet s
μs : μ s ≠ ∞
r : ℝ≥0∞
hr : r < μ s
⊢ ∃ K ⊆ s, (fun s ↦ IsCompact s ∧ IsClosed[inst✝³] s) K ∧ r < μ K
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
⊢ μ' s * ν' t = ν' s * μ' t

Tactic:
have h1 := 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 ∂ν'
⊢ μ' s * ν' t = ν' s * μ' t
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
s : Set G
hs : MeasurableSet s
⊢ μ s = 0 → (map (fun h ↦ h * g) μ) s = 0

Tactic:
map_apply (measurable_mul_const g) hs,

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
s : Set G
hs : MeasurableSet s
⊢ μ s = 0 → μ ((fun x ↦ x * g) ⁻¹' s) = 0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝¹ : MeasurableSpace β
f : β → α → ℝ≥0∞
inst✝ : SFinite μ
hf : Measurable (Function.uncurry f)
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b ↦ (μ.withDensity (f b)) s

Tactic:
simp only [withDensity_apply _ hs]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝¹ : MeasurableSpace β
f : β → α → ℝ≥0∞
inst✝ : SFinite μ
hf : Measurable (Function.uncurry f)
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b ↦ ∫⁻ (a : α) in s, f b a ∂μ
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
ε : Type u_4
ε' : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : ENorm ε
inst✝ : ENorm ε'
f : α → ε
g : α → ε'
hg : HasFiniteIntegral g μ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ ‖g a‖ₑ
⊢ HasFiniteIntegral f μ

Tactic:
simp only [hasFiniteIntegral_iff_enorm] at *

Goal state after:
α : Type u_1
ε : Type u_4
ε' : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : ENorm ε
inst✝ : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ ‖g a‖ₑ
hg : ∫⁻ (a : α), ‖g a‖ₑ ∂μ < ∞
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
x : α
⊢ ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal

Tactic:
Real.enorm_of_nonneg ENNReal.toReal_nonneg

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
x : α
⊢ ENNReal.ofReal (f x).toReal = ENNReal.ofReal (f x).toReal
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
F_le_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)
⊢ ∀ (x : α),
    Tendsto (fun n ↦ ENNReal.ofReal ‖F n x‖) atTop (𝓝 (ENNReal.ofReal ‖f x‖)) →
      (∀ (i : ℕ), ENNReal.ofReal ‖F i x‖ ≤ ENNReal.ofReal (bound x)) → ENNReal.ofReal ‖f x‖ ≤ ENNReal.ofReal (bound x)

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
F_le_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)
a : α
⊢ Tendsto (fun n ↦ ENNReal.ofReal ‖F n a‖) atTop (𝓝 (ENNReal.ofReal ‖f a‖)) →
    (∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)) → ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
F' : ℕ → α → ε
f' : α → ε
bound' : α → ℝ≥0∞
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ‖F' i a‖ₑ ≤ bound' a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F' n a) atTop (𝓝 (f' a))
⊢ ∀ (x : α), Tendsto (fun n ↦ ‖F' n x‖ₑ) atTop (𝓝 ‖f' x‖ₑ) → (∀ (i : ℕ), ‖F' i x‖ₑ ≤ bound' x) → ‖f' x‖ₑ ≤ bound' x

Tactic:
intro a

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
F' : ℕ → α → ε
f' : α → ε
bound' : α → ℝ≥0∞
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ‖F' i a‖ₑ ≤ bound' a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F' n a) atTop (𝓝 (f' a))
a : α
⊢ Tendsto (fun n ↦ ‖F' n a‖ₑ) atTop (𝓝 ‖f' a‖ₑ) → (∀ (i : ℕ), ‖F' i a‖ₑ ≤ bound' a) → ‖f' a‖ₑ ≤ bound' a
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ √x < y ↔ x < y ^ 2

Tactic:
← sqrt_lt_sqrt_iff hx,

Goal state after:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ √x < y ↔ √x < √(y ^ 2)
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
⊢ √x ^ 2 = max x 0

Tactic:
by
  rcases lt_trichotomy x 0 with _ | _ | _ <;> grind [sqrt_eq_zero', sq_sqrt]

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

Goal state before:
pp: ⊢ √2 < 3 / 2

Tactic:
rw [← sq_lt_sq₀ (by positivity) (by positivity)]

Goal state after:
⊢ √2 ^ 2 < (3 / 2) ^ 2
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
⊢ ∀ (r s : ↥(unitary R)), star (r * s) = star s * star r

Tactic:
intro x y
    ext
    rw [coe_star, Submonoid.coe_mul, Submonoid.coe_mul, coe_star, coe_star, star_mul]

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

Goal state before:
pp: case zero
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
⊢ ‖x ^ 2 ^ 0‖₊ = ‖x‖₊ ^ 2 ^ 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : Group α
inst✝ : MulAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
⊢ ∀ (a : α), π (a • b) = π b

Tactic:
intro a

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : Group α
inst✝ : MulAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
a : α
⊢ π (a • b) = π b
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: f : ℂ →ₐ[ℝ] ℂ
⊢ f I ^ 2 = I ^ 2

Tactic:
rw [← map_pow, I_sq, map_neg, map_one]

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

Goal state before:
pp: ζ : ℂ
n : ℕ
h : ζ ^ n = 1
hn : n ≠ 0
⊢ ‖ζ‖₊ ^ n = 1 ^ n

Tactic:
rw [← nnnorm_pow, h, nnnorm_one, one_pow]

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (Algebra.linearMap ℝ A ∘ₗ reLm + LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm)
      { re := x₁ * x₂ - y₁ * y₂, im := x₁ * y₂ + y₁ * x₂ } =
    (Algebra.linearMap ℝ A ∘ₗ reLm + LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) { re := x₁, im := y₁ } *
      (Algebra.linearMap ℝ A ∘ₗ reLm + LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) { re := x₂, im := y₂ }

Tactic:
change
    algebraMap ℝ A (x₁ * x₂ - y₁ * y₂) + (x₁ * y₂ + y₁ * x₂) • I' =
      (algebraMap ℝ A x₁ + y₁ • I') * (algebraMap ℝ A x₂ + y₂ • I')

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) + (x₁ * y₂ + y₁ * x₂) • I' =
    ((algebraMap ℝ A) x₁ + y₁ • I') * ((algebraMap ℝ A) x₂ + y₂ • I')
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: x : ℂ
⊢ x.im = 0 ↔ IsSelfAdjoint x

Tactic:
by
  rw [← RCLike.im_eq_complex_im]
  exact RCLike.im_eq_zero_iff_isSelfAdjoint

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
⊢ ∀ (x y : ℝ), (algebraMap ℝ 𝕜) (x * y) = (algebraMap ℝ 𝕜) x * (algebraMap ℝ 𝕜) y

Tactic:
exact h.algebraMap.map_mul'

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

Goal state before:
pp: α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ c⁻¹ * ‖f x‖ ≤ ‖g x‖

Tactic:
rwa [inv_mul_le_iff₀ (by positivity)]

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

Goal state before:
pp: n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ List.range ↑nn = 0 :: List.map Nat.succ (List.range n')

Tactic:
Nat.cast_id,

Goal state after:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ List.range nn = 0 :: List.map Nat.succ (List.range n')
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ Multiset.range ↑nn = n' ::ₘ Multiset.range n'

Tactic:
Nat.cast_id,

Goal state after:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ Multiset.range nn = n' ::ₘ Multiset.range n'
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ Finset.range ↑nn = Finset.cons n' (Finset.range n') ⋯

Tactic:
Nat.cast_id,

Goal state after:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ Finset.range nn = Finset.cons n' (Finset.range n') ⋯
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
c₁ c₂ : ℝ
h₁ : IsBigOWith c₁ l f₁ g₁
h₂ : IsBigOWith c₂ l f₂ g₂
⊢ IsBigOWith (c₁ * c₂) l (fun x ↦ f₁ x * f₂ x) fun x ↦ g₁ x * g₂ x

Tactic:
simp only [IsBigOWith_def] at *
  filter_upwards [h₁, h₂] with _ hx₁ hx₂
  apply le_trans (norm_mul_le _ _)
  convert! mul_le_mul hx₁ hx₂ (norm_nonneg _) (le_trans (norm_nonneg _) hx₁) using 1
  rw [norm_mul, mul_mul_mul_comm]

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

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
i : ℕ
⊢ abv (∑ i ∈ range (0 + max n i), f i - ∑ i ∈ range (max n i), f i) ≤
    ∑ k ∈ range (0 + max n i), a k - ∑ k ∈ range (max n i), a k

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f : α → R
g : α → S
h : f =o[l] g
⊢ (fun x ↦ f x ^ Nat.succ 0) =o[l] fun x ↦ g x ^ Nat.succ 0

Tactic:
| zero =>

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

Goal state before:
pp: case succ.zero
ε : ℝ
ε0 : ε > 0
hj : 0 + 1 ≥ 1
⊢ ‖∑ m ∈ range (0 + 1), 0 ^ m / ↑m.factorial - 1‖ = 0

Tactic:
| zero =>

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

Goal state before:
pp: x : ℂ
⊢ sinh x - cosh x = -cexp (-x)

Tactic:
rw [← neg_sub, cosh_sub_sinh]

Goal state after:
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:
rw [isBigOWith_iff, 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‖) ↔ ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: case inl
x : ℝ
h✝ : x ≤ 0
⊢ cos |x| = cos x

Tactic:
simp only [*, abs_of_nonneg, abs_of_nonpos, cos_neg]

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

Goal state before:
pp: case inr
x : ℝ
h✝ : 0 ≤ x
⊢ cos |x| = cos x

Tactic:
simp only [*, abs_of_nonneg, abs_of_nonpos, cos_neg]

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

Goal state before:
pp: x y : ℝ
⊢ ↑(sin x - sin y) = ↑(2 * sin ((x - y) / 2) * cos ((x + y) / 2))

Tactic:
by simp [sin_sub_sin]

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

Goal state before:
pp: x : ℝ
⊢ sinh x - cosh x = -rexp (-x)

Tactic:
rw [← neg_sub, cosh_sub_sinh]

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

Goal state before:
pp: E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h✝ : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec✝ :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun n ↦ ‖f n‖ / ‖g n‖
m : ℕ
hm : m ∈ Finset.Icc n₀ n₁
⊢ ‖f m‖ = ‖f m‖ / ‖g m‖ * ‖g m‖

Tactic:
by_cases hm' : g m = 0 <;> grind [norm_eq_zero]

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f : ι → R
g : ι' → R
hf : Summable fun x ↦ ‖f x‖
h'f : Summable f
hg : Summable fun x ↦ ‖g x‖
h'g : Summable g
s : Finset ι × Finset ι' → Finset (ι × ι') := fun p ↦ p.1 ×ˢ p.2
this :
  Tendsto (Prod.map (fun s ↦ ∑ b ∈ s, f b) fun s ↦ ∑ b ∈ s, g b)
    ((SummationFilter.unconditional ι).filter ×ˢ (SummationFilter.unconditional ι').filter)
    (𝓝 (∑' (b : ι), f b) ×ˢ 𝓝 (∑' (b : ι'), g b))
⊢ Tendsto (fun b ↦ ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2) (atTop ×ˢ atTop) (𝓝 ((∑' (i : ι), f i) * ∑' (j : ι'), g j))

Tactic:
← nhds_prod_eq

Goal state after:
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f : ι → R
g : ι' → R
hf : Summable fun x ↦ ‖f x‖
h'f : Summable f
hg : Summable fun x ↦ ‖g x‖
h'g : Summable g
s : Finset ι × Finset ι' → Finset (ι × ι') := fun p ↦ p.1 ×ˢ p.2
this :
  Tendsto (Prod.map (fun s ↦ ∑ b ∈ s, f b) fun s ↦ ∑ b ∈ s, g b)
    ((SummationFilter.unconditional ι).filter ×ˢ (SummationFilter.unconditional ι').filter)
    (𝓝 (∑' (b : ι), f b, ∑' (b : ι'), g b))
⊢ Tendsto (fun b ↦ ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2) (atTop ×ˢ atTop) (𝓝 ((∑' (i : ι), f i) * ∑' (j : ι'), g j))
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case inr.inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
h' : 1 ≤ -x
⊢ x + 1 < rexp x

pp: case inr.inr
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
h' : -x < 1
⊢ x + 1 < rexp x

Tactic:
· linarith [x.exp_pos]

Goal state after:
case inr.inr
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
h' : -x < 1
⊢ x + 1 < rexp x
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: A : Tendsto (fun x ↦ x + 1) atTop atTop
B : ∀ᶠ (x : ℝ) in atTop, x + 1 ≤ rexp x
⊢ Tendsto rexp atTop atTop

Tactic:
exact tendsto_atTop_mono' atTop B A

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

Goal state before:
pp: case inr.zero
α : 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
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = 0 + n.succ
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m

Tactic:
| zero =>

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

Goal state before:
pp: ⊢ 1 ≤ Classical.choose exists_cos_eq_zero

Tactic:
exact (Classical.choose_spec exists_cos_eq_zero).1.1

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

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ
⊢ ((fun x ↦ rexp (f x)) =O[l] fun x ↦ 1) ↔ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l f

Tactic:
by
  simp only [isBigO_one_iff, norm_eq_abs, abs_exp, isBoundedUnder_le_exp_comp]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ ‖x - (r • x + (1 - r) • y)‖ = ‖1 - r‖ * ‖x - y‖

Tactic:
← norm_smul,

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ ‖x - (r • x + (1 - r) • y)‖ = ‖(1 - r) • (x - y)‖