mathlib-initiative/mathlib-tactics huggingface dataset:
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 μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable fun y ↦ ((fun z ↦ z * x) ⁻¹' s).indicator (fun x ↦ 1) y
this : ∀ (x y : G), s.indicator (fun x ↦ 1) (y * x) = ((fun z ↦ z * x) ⁻¹' s).indicator (fun b ↦ 1) y
⊢ ∫⁻ (x : G), (∫⁻ (a : G), ((fun z ↦ z * x) ⁻¹' s).indicator (fun x ↦ 1) a ∂ν) * f x⁻¹ ∂μ =
    ∫⁻ (x : G), ν ((fun z ↦ z * x) ⁻¹' s) * f x⁻¹ ∂μ

Tactic:
lintegral_indicator (measurable_mul_const _ sm),

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
s : Set G
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
sm : MeasurableSet s
f : G → ℝ≥0∞
hf : Measurable f
ms : ∀ (x : G), Measurable fun y ↦ ((fun z ↦ z * x) ⁻¹' s).indicator (fun x ↦ 1) y
this : ∀ (x y : G), s.indicator (fun x ↦ 1) (y * x) = ((fun z ↦ z * x) ⁻¹' s).indicator (fun b ↦ 1) y
⊢ ∫⁻ (x : G), (∫⁻ (x : G) in (fun z ↦ z * x) ⁻¹' s, 1 ∂ν) * f x⁻¹ ∂μ = ∫⁻ (x : G), ν ((fun z ↦ z * x) ⁻¹' s) * f x⁻¹ ∂μ
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁴] K
hμK : μ (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst✝⁴] U
hμU : μ U < μ K + ε / 2
⊢ μ (U \ K) < ε / 2

Tactic:
by
        apply measure_sdiff_lt_of_lt_add hKcl.nullMeasurableSet hKU _ hμU
        exact ne_top_of_le_ne_top hμs (by gcongr)

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

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
x : α
hx : x ∈ s
fx : f x ≠ 0
⊢ x ∈ t ∪ {x | f x = 0}

Tactic:
· left
        apply subset_toMeasurable _ _
        exact ⟨fx, hx⟩

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : ¬c = 0
h'c : c = ∞
s : Set α
hs : MeasurableSet s ∧ (c • μ) s ≠ ∞
r : ℝ≥0∞
hr : r < (c • μ) s
h's : ¬μ s = 0
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (c • μ) K

Tactic:
simp [h'c, h's] at hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
⊢ HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ < ∞

Tactic:
simp only [hasFiniteIntegral_iff_enorm, ofReal_norm]

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

Goal state before:
pp: x : ℝ
h : 0 ≤ x
⊢ √x = 0 ↔ x = 0

Tactic:
simpa using sqrt_inj h le_rfl

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

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

Tactic:
sqrt_le_iff,

Goal state after:
x : ℝ
⊢ 0 ≤ x ∧ x ≤ x ^ 2 ↔ x = 0 ∨ 1 ≤ x
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
⊢ z.im ^ 2 ≤ normSq z

Tactic:
rw [normSq_apply, ← sq, ← sq]
    exact le_add_of_nonneg_left (sq_nonneg _)

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

Goal state before:
pp: x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ √(x ^ 2 + y ^ 2) ≤ √(m ^ 2 + m ^ 2)

Tactic:
gcongr √(?_ + ?_) <;> rw [sq_le_sq, abs_of_nonneg hm₀]
      exacts [le_max_left _ _, le_max_right _ _]

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

Goal state before:
pp: x✝ : ℂ
⊢ 0 • x✝ = 0

Tactic:
ext <;> simp [smul_re, smul_im]

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

Goal state before:
pp: n✝ : ℕ
x✝ : ℂ
⊢ (n✝ + 1) • x✝ = n✝ • x✝ + x✝

Tactic:
ext <;> simp [smul_re, smul_im]

Goal state after:
case a
n✝ : ℕ
x✝ : ℂ
⊢ (↑n✝ + 1) * x✝.re = ↑n✝ * x✝.re + x✝.re

case a
n✝ : ℕ
x✝ : ℂ
⊢ (↑n✝ + 1) * x✝.im = ↑n✝ * x✝.im + x✝.im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: a✝ : ℂ
⊢ 0 • a✝ = 0

Tactic:
ext <;> simp [smul_re, smul_im]

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

Goal state before:
pp: n✝ : ℕ
a✝ : ℂ
⊢ ↑n✝.succ • a✝ = ↑n✝ • a✝ + a✝

Tactic:
ext <;> simp [smul_re, smul_im]

Goal state after:
case a
n✝ : ℕ
a✝ : ℂ
⊢ (↑n✝ + 1) * a✝.re = ↑n✝ * a✝.re + a✝.re

case a
n✝ : ℕ
a✝ : ℂ
⊢ (↑n✝ + 1) * a✝.im = ↑n✝ * a✝.im + a✝.im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: n✝ : ℕ
a✝ : ℂ
⊢ Int.negSucc n✝ • a✝ = -(↑n✝.succ • a✝)

Tactic:
ext <;> simp [smul_re, smul_im]

Goal state after:
case a
n✝ : ℕ
a✝ : ℂ
⊢ (-1 + -↑n✝) * a✝.re = -((↑n✝ + 1) * a✝.re)

case a
n✝ : ℕ
a✝ : ℂ
⊢ (-1 + -↑n✝) * a✝.im = -((↑n✝ + 1) * a✝.im)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ I ^ 3 = -I

Tactic:
rw [pow_succ, I_sq, neg_one_mul]

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

Goal state before:
pp: z : ℂ
⊢ z⁻¹.re = z.re / normSq z

Tactic:
by simp [inv_def, division_def, ofReal]

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

Goal state before:
pp: z : ℂ
⊢ z⁻¹.im = -z.im / normSq z

Tactic:
by simp [inv_def, division_def, ofReal]

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 φ
⊢ ∫⁻ (y : G), ∫⁻ (x : G), ((fun z ↦ f z.1 * g z.2) * fun z ↦ φ (z.1 * z.2)) (x, x⁻¹ * y) ∂μ ∂μ =
    ∫⁻ (a : G), ((f ⋆ₘₗ[μ] g) * φ) a ∂μ

Tactic:
simp only [Pi.mul_apply, mul_inv_cancel_left, mlconvolution_def]
    conv in (∫⁻ _, _ ∂μ) * φ _ => rw [(lintegral_mul_const'' _ (by fun_prop)).symm]

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 : ℂ
⊢ r • x = (ofRealHom.comp (algebraMap R ℝ)) r * x

Tactic:
ext <;> simp [smul_re, smul_im, Algebra.smul_def]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
⊢ ∃ c, ‖c‖ = 1 ∧ ↑‖x‖ = c * x

Tactic:
obtain rfl | hx := eq_or_ne x 0

Goal state after:
case inl
K : Type u_1
inst✝ : RCLike K
⊢ ∃ c, ‖c‖ = 1 ∧ ↑‖0‖ = c * 0

case inr
K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ∃ c, ‖c‖ = 1 ∧ ↑‖x‖ = c * x
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
⊢ ∃ c, ‖c‖ = 1 ∧ c * ↑‖x‖ = x

Tactic:
obtain rfl | hx := eq_or_ne x 0

Goal state after:
case inl
K : Type u_1
inst✝ : RCLike K
⊢ ∃ c, ‖c‖ = 1 ∧ c * ↑‖0‖ = 0

case inr
K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ∃ c, ‖c‖ = 1 ∧ c * ↑‖x‖ = x
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: case left
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ IsInducing (e.source.domRestrict ↑e.toPartialEquiv)

Tactic:
apply Topology.IsInducing.of_codRestrict (t := e.target) (by simp)

Goal state after:
case left
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ IsInducing (codRestrict (e.source.domRestrict ↑e.toPartialEquiv) e.target ⋯)
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
s : Set X
t : Set Z
x : X
f : X → Z
hf : ContinuousWithinAt f s x
hxe : x ∈ e.source
ht : t ∈ 𝓝 (f x)
⊢ ↑e.symm ⁻¹' s =ᶠ[𝓝 (↑e x)] e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)

Tactic:
rw [eventuallyEq_set, e.eventually_nhds _ hxe]
  filter_upwards [e.open_source.mem_nhds hxe,
    mem_nhdsWithin_iff_eventually.mp (hf.preimage_mem_nhdsWithin ht)]
  intro y hy hyu
  simp_rw [mem_inter_iff, mem_preimage, mem_inter_iff, e.mapsTo hy, true_and, iff_self_and,
    e.left_inv hy, iff_true_intro hyu]

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
⊢ (algebraMap ℝ 𝕜) 1 = 1

Tactic:
subst h''; exact h.algebraMap.map_one'

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

Goal state before:
pp: z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
⊢ ‖z‖ / ↑n < 1

Tactic:
by rwa [div_lt_iff₀ hn0, one_mul]

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

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

Tactic:
neg_add,

Goal state after:
x y : ℂ
⊢ cexp x * cexp y - cexp (-x + -y) = 2 * (sinh x * cosh y + cosh x * sinh y)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
neg_add,

Goal state after:
x y : ℂ
⊢ cexp x * cexp y + cexp (-x + -y) = 2 * (cosh x * cosh y + sinh x * sinh y)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: ⊢ rexp 0 = 1

Tactic:
by simp [Real.exp]

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

Goal state before:
pp: x : ℂ
⊢ ((starRingEnd ℂ) x).cot = (starRingEnd ℂ) x.cot

Tactic:
by rw [cot, sin_conj, cos_conj, ← map_div₀, cot]

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

Goal state before:
pp: x : ℝ
⊢ (cexp (↑x * I)).im = Real.sin x

Tactic:
by
  simp [exp_mul_I, sin_ofReal_re]

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

Goal state before:
pp: n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : |x| ≤ 1
⊢ |rexp x - ∑ m ∈ range m, x ^ m / ↑m.factorial| ≤ |x| ^ m / ↑m.factorial * ((↑m + 1) / ↑m)

Tactic:
convert! exp_bound (n := m) h ?_ using 1

Goal state after:
n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : |x| ≤ 1
⊢ |x| ^ m / ↑m.factorial * ((↑m + 1) / ↑m) = |x| ^ m * (↑m.succ / (↑m.factorial * ↑m))

n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : |x| ≤ 1
⊢ 0 < m
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : |1 + x / ↑(n + 1) * a₂ - a₁| ≤ b₁ - |x| / ↑(n + 1) * b₂
h : |rexp x - expNear (n + 1) x a₂| ≤ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂
⊢ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂ + |expNear (n + 1) x a₂ - expNear n x a₁| ≤ |x| ^ n / ↑n.factorial * b₁

Tactic:
rw [expNear_succ, expNear_sub, abs_mul]

Goal state after:
n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : |1 + x / ↑(n + 1) * a₂ - a₁| ≤ b₁ - |x| / ↑(n + 1) * b₂
h : |rexp x - expNear (n + 1) x a₂| ≤ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂
⊢ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂ + |x ^ n / ↑n.factorial| * |1 + x / (↑n + 1) * a₂ - a₁| ≤
    |x| ^ n / ↑n.factorial * b₁
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

Tactic:
linarith [x.exp_pos]

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

Goal state before:
pp: x : ℝ
⊢ x + 1 ≤ rexp x

Tactic:
obtain rfl | hx := eq_or_ne x 0

Goal state after:
case inl
⊢ 0 + 1 ≤ rexp 0

case inr
x : ℝ
hx : x ≠ 0
⊢ x + 1 ≤ rexp x
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
⊢ k + n.succ ≥ n.succ

Tactic:
rw [← zero_add n.succ]

Goal state after:
α : 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
⊢ k + (0 + n.succ) ≥ 0 + n.succ
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: case a
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
⊢ ↑⌈x⌉₊ ≤ x + 1

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

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

Goal state before:
pp: ⊢ Set.range rexp = Set.Ioi 0

Tactic:
← coe_comp_expOrderIso,

Goal state after:
⊢ Set.range (Subtype.val ∘ ⇑expOrderIso) = Set.Ioi 0
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: a : ℝ
⊢ rexp '' Set.Iio a = Set.Ioo 0 (rexp a)

Tactic:
← coe_comp_expOrderIso,

Goal state after:
a : ℝ
⊢ Subtype.val ∘ ⇑expOrderIso '' Set.Iio a = Set.Ioo 0 ((Subtype.val ∘ ⇑expOrderIso) a)
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: a : ℝ
⊢ rexp '' Set.Iic a = Set.Ioc 0 (rexp a)

Tactic:
← coe_comp_expOrderIso,

Goal state after:
a : ℝ
⊢ Subtype.val ∘ ⇑expOrderIso '' Set.Iic a = Set.Ioc 0 ((Subtype.val ∘ ⇑expOrderIso) a)
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: ⊢ Filter.map rexp atTop = atTop

Tactic:
← coe_comp_expOrderIso,

Goal state after:
⊢ Filter.map (Subtype.val ∘ ⇑expOrderIso) atTop = atTop
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: ⊢ Filter.map rexp atBot = 𝓝[>] 0

Tactic:
← coe_comp_expOrderIso,

Goal state after:
⊢ Filter.map (Subtype.val ∘ ⇑expOrderIso) atBot = 𝓝[>] 0
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 ε : ℝ
h : S ≤ T
⊢ Isometry ⇑(quotientQuotientEquivQuotient S T h)

Tactic:
by
    rw [MonoidHomClass.isometry_iff_norm]
    refine fun x => eq_of_forall_le_iff fun r => ?_
    simp only [le_norm_iff]
    exact ⟨
      fun h₁ y h₂ z h₃ => h₁ z <| by subst_vars; rfl,
      fun h₁ y h₂ => h₁ y ((quotientQuotientEquivQuotient S T h).injective h₂) y rfl⟩

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

Goal state before:
pp: x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
⊢ cos y < cos x

Tactic:
rw [← sin_pi_div_two_sub, ← sin_pi_div_two_sub]
  apply sin_lt_sin_of_lt_of_le_pi_div_two <;> linarith

Goal state after:
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
⊢ (sphere x r).Nonempty

Tactic:
obtain ⟨y, hy⟩ := exists_norm_eq E hr

Goal state after:
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NontrivialTopology E
x : E
r : ℝ
hr : 0 ≤ r
y : E
hy : ‖y‖ = r
⊢ (sphere x r).Nonempty
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 8) = √(2 + √2) / 2

Tactic:
trans cos (π / 2 ^ 3)
  · congr
    norm_num
  · simp

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 : 𝕜
hc : c ∈ s
⊢ c • sphere 0 r = sphere 0 (‖c‖ * r)

Tactic:
rw [smul_sphere' (ne_of_mem_of_not_mem hc hs), smul_zero]

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

Goal state before:
pp: case inr
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
⊢ cos (π / 3) = 1 / 2

Tactic:
have : cos π < cos (π / 3) := by
      refine cos_lt_cos_of_nonneg_of_le_pi ?_ le_rfl ?_ <;> linarith [pi_pos]
    linarith [cos_pi]

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

Goal state before:
pp: ⊢ tan (π / 3) = √3

Tactic:
by
  rw [tan_eq_sin_div_cos, sin_pi_div_three, cos_pi_div_three]
  ring

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

Goal state before:
pp: R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n ↦ ↑(u n)) =O[atTop] fun n ↦ ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ (fun n ↦ ‖↑(u n) * r ^ n‖) =O[atTop] fun n ↦ ↑(u n) * ‖r‖ ^ n

Tactic:
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))

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

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k : ℕ
r : R
hr : ‖r‖ < 1
⊢ Summable fun n ↦ ↑n ^ k * r ^ n

Tactic:
refine Nat.strong_induction_on k fun k hk => ?_
  obtain ⟨a, ha⟩ : ∃ (a : ℕ → ℕ), ∀ n, (n + k).descFactorial k
      = n ^ k + ∑ i ∈ range k, a i * n ^ i := by
    let P : Polynomial ℕ := (ascPochhammer ℕ k).comp (Polynomial.X + C 1)
    refine ⟨fun i ↦ P.coeff i, fun n ↦ ?_⟩
    have mP : Monic P := Monic.comp_X_add_C (monic_ascPochhammer ℕ k) _
    have dP : P.natDegree = k := by
      simp only [P, natDegree_comp, ascPochhammer_natDegree, mul_one, natDegree_X_add_C]
    have A : (n + k).descFactorial k = P.eval n := by
      have : n + 1 + k - 1 = n + k := by lia
      simp [P, ascPochhammer_nat_eq_descFactorial, this]
    conv_lhs => rw [A, mP.as_sum, dP]
    simp [eval_finsetSum]
  have : Summable (fun n ↦ (n + k).descFactorial k * r ^ n
      - ∑ i ∈ range k, a i * n ^ (i : ℕ) * r ^ n) := by
    apply (summable_descFactorial_mul_geometric_of_norm_lt_one k hr).sub
    apply summable_sum (fun i hi ↦ ?_)
    simp_rw [mul_assoc]
    simp only [Finset.mem_range] at hi
    exact (hk _ hi).mul_left _
  convert! this using 1
  ext n
  simp [ha n, add_mul, sum_mul]

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ ofLine ⋯ ⋯ ⋯ = γ

Tactic:
by
  ext t
  simp [ofLine]

Goal state after:
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‖
⊢ Summable fun n ↦ f n * z ^ n

Tactic:
obtain ⟨C, hC⟩ := exists_norm_le_of_cauchySeq h

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
⊢ Summable fun n ↦ f n * z ^ n
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:
rw [norm_mul, norm_pow, ← _root_.le_div_iff₀ (by positivity)]

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.Topology.Instances.ZMultiples

Goal state before:
pp: a : ℝ
⊢ IsDiscrete ↑(zmultiples a)

Tactic:
rw [SetLike.isDiscrete_iff_discreteTopology]

Goal state after:
a : ℝ
⊢ DiscreteTopology ↥(zmultiples a)
Module: Mathlib.Topology.Instances.AddCircle.Real

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
⊢ ∀ (a b : ℤ), ↑(↑(a + b) / ↑N) = ↑(↑a / ↑N) + ↑(↑b / ↑N)

Tactic:
simp [add_div]

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: case refine_1
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ₂
h₁' : Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ₁ t).extend
h₂' : Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ₂ t).extend
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] ((fun p ↦ (γ₁ p.1).extend p.2) ∘ Prod.map id fun x ↦ 2 * ↑x)

Tactic:
exact h₁'.comp (by fun_prop)

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

Goal state before:
pp: E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n ↦
    f n • ∑ i ∈ Finset.range n.succ, z i + -∑ x ∈ Finset.range n, (f (x + 1) + -f x) • ∑ i ∈ Finset.range (x + 1), z i

Tactic:
apply (NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded hf0
    ⟨b, eventually_map.mpr <| Eventually.of_forall fun n ↦ hgb <| n + 1⟩).cauchySeq.add

Goal state after:
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n ↦ -∑ x ∈ Finset.range n, (f (x + 1) + -f x) • ∑ i ∈ Finset.range (x + 1), z i
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 ≤
    ∑ x ∈ Finset.range (2 * n + 1 + 1), (-1) ^ x * f x + (-1) ^ (2 * n + 1 + 1) * f (2 * n + 1 + 1)

Tactic:
sum_range_succ _ (2 * n + 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) ^ x * f x + (-1) ^ (2 * n + 1) * f (2 * n + 1) +
      (-1) ^ (2 * n + 1 + 1) * f (2 * n + 1 + 1)
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) ^ i * f i + f (2 * n + 1 + 1) - f (2 * n + 1)

Tactic:
le_sub_iff_add_le

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 + f (2 * n + 1) ≤
    ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i + f (2 * n + 1 + 1)