mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case inr.refine_2
X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
x : X
C : Set X
hxC : C ∈ 𝓝 x
ε : ℝ := min (infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)) 1
hC : (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ).Nonempty
this✝ : Nonempty X
n : ℕ
hn : dist x (denseSeq X n) < ε / 2
y : X
hy : dist y (denseSeq X n) < ε / 2
this : dist x y < infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Cᶜ)
⊢ y ∈ C

Tactic:
simpa using notMem_of_notMem_closure (mt infDist_le_dist_of_mem this.not_ge)

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : PolishSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T0Space Y
inst✝ : SecondCountableTopology Y
f : X → Y
hf : Continuous[inst✝⁶, inst✝²] f
hsurj : Surjective f
⊢ MeasurableSpace.map f inst✝⁴ = borel Y

Tactic:
borelize Y
  exact hf.measurable.map_measurableSpace_eq hsurj

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α → β
hf : AEMeasurable f μ
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (f '' K)
hB₂ : ∀ (U : Set β), qb U → MeasurableSet U
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < (map f μ) U
⊢ ∃ K ⊆ U, pb K ∧ r < (map f μ) K

Tactic:
rw [map_apply_of_aemeasurable hf (hB₂ _ hU)] at hr

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α → β
hf : AEMeasurable f μ
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (f '' K)
hB₂ : ∀ (U : Set β), qb U → MeasurableSet U
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < μ (f ⁻¹' U)
⊢ ∃ K ⊆ U, pb K ∧ r < (map f μ) K
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement S ↑H''
⊢ Nat.card ↑(⇑H.subtype '' S) * Nat.card ↥(map H.subtype H'') = Nat.card ↥H

Tactic:
· rw [← cmem.card_mul_card]
    refine congr_arg₂ (· * ·) ?_ ?_ <;>
      exact Nat.card_congr (Equiv.Set.image _ _ <| subtype_injective H).symm

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
f : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
q : Quotient (QuotientGroup.rightRel H)
⊢ ↑(⋯.rightQuotientEquiv q) = f q

Tactic:
by
  refine (Subtype.ext_iff.mp ?_).trans (Subtype.coe_mk (f q) ⟨q, rfl⟩)
  exact (rightQuotientEquiv (isComplement_range_right hf)).eq_symm_apply.1 (hf q).symm

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

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
ν : Measure α
inst✝¹ : μ.OuterRegular
inst✝ : ν.OuterRegular
hμν : ∀ (U : Set α), IsOpen[inst✝²] U → μ U = ν U
⊢ μ = ν

Tactic:
ext s ms

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
ν : Measure α
inst✝¹ : μ.OuterRegular
inst✝ : ν.OuterRegular
hμν : ∀ (U : Set α), IsOpen[inst✝²] U → μ U = ν U
s : Set α
ms : MeasurableSet s
⊢ μ s = ν s
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ μ (s ∆ (c⁻¹ • t)) = μ ((c • s) ∆ t)

Tactic:
by
  rw [← measure_smul _ c, smul_set_symmDiff, smul_smul, mul_inv_cancel, one_smul]

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

Goal state before:
pp: M : Type uM
α : Type uα
β : Type uβ
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : MeasurableConstSMul M β
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
f : α → β
hsmul : ∀ (m : M) (a : α), f (m • a) = m • f a
hf : Measurable f
m : M
S : Set β
hS : MeasurableSet S
⊢ μ ((fun x ↦ m • f x) ⁻¹' S) = μ ((fun x ↦ f (m • x)) ⁻¹' S)

Tactic:
hsmul

Goal state after:
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 μ
this :
  (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) =
    sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))
i : ℕ × ℕ
s : Set β
t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)) (Prod.swap ⁻¹' s ×ˢ t) = (sfiniteSeq ν i.1) s * (sfiniteSeq μ i.2) t

Tactic:
preimage_swap_prod,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
this :
  (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) =
    sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))
i : ℕ × ℕ
s : Set β
t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)) (t ×ˢ s) = (sfiniteSeq ν i.1) s * (sfiniteSeq μ i.2) t
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 μ
μ' : Measure α
inst✝ : SFinite μ'
i : ℕ × ℕ
s : Set α
t : Set β
x✝¹ : MeasurableSet s
x✝ : MeasurableSet t
⊢ ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2) + (sfiniteSeq μ' i.1).prod (sfiniteSeq ν i.2)) (s ×ˢ t) =
    (sfiniteSeq μ i.1 + sfiniteSeq μ' i.1) s * (sfiniteSeq ν i.2) t

Tactic:
simp_rw [add_apply, prod_prod, right_distrib]

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

Goal state before:
pp: case map_eq.inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
δ : Type u_4
inst✝² : MeasurableSpace δ
μb : Measure β
μc : Measure γ
μd : Measure δ
inst✝¹ : SFinite μc
f : α → β
g : α → γ → δ
hgm : Measurable (uncurry g)
this : Measurable fun p ↦ (f p.1, g p.1 p.2)
inst✝ : SFinite 0
hf : MeasurePreserving f 0 μb
hg : ∀ᵐ (a : α) ∂0, map (g a) μc = μd
⊢ map (fun p ↦ (f p.1, g p.1 p.2)) (Measure.prod 0 μc) = μb.prod μd

Tactic:
simp [← hf.map_eq]

Goal state after:
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✝ : μ.IsMulLeftInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
x✝ : H
⊢ x✝ ∈ (fun x ↦ f g * x) ⁻¹' ⇑f '' s → x✝ ∈ ⇑f '' (fun x ↦ g * x) ⁻¹' s

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : IsProbabilityMeasure μ
s : Set β
hs : MeasurableSet s
⊢ (μ.prod ν).snd s = ν s

Tactic:
snd_apply hs,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : IsProbabilityMeasure μ
s : Set β
hs : MeasurableSet s
⊢ (μ.prod ν) (Prod.snd ⁻¹' s) = ν s
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
⊢ ∫⁻ (x : G), ∫⁻ (y : G), f (y * x) x⁻¹ ∂ν ∂μ = ∫⁻ (x : G), ∫⁻ (y : G), f x y ∂ν ∂μ

Tactic:
by
  have h : Measurable fun z : G × G => (z.2 * z.1, z.1⁻¹) :=
    (measurable_snd.mul measurable_fst).prodMk measurable_fst.inv
  have h2f : AEMeasurable (uncurry fun x y => f (y * x) x⁻¹) (μ.prod ν) :=
    hf.comp_quasiMeasurePreserving (measurePreserving_mul_prod_inv μ ν).quasiMeasurePreserving
  simp_rw [lintegral_lintegral h2f, lintegral_lintegral hf]
  conv_rhs => rw [← (measurePreserving_mul_prod_inv μ ν).map_eq]
  symm
  exact
    lintegral_map' (hf.mono' (measurePreserving_mul_prod_inv μ ν).map_eq.absolutelyContinuous)
      h.aemeasurable

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
⊢ (μ + ν).withDensity f = μ.withDensity f + ν.withDensity f

Tactic:
ext1 s hs
  simp only [withDensity_apply f hs, restrict_add, lintegral_add_measure, Measure.add_apply]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g : ℕ → α → ℝ≥0∞
h_mea_g : ∀ (n : ℕ), Measurable (g n)
h_mono_g : Monotone g
h_ind : ∀ (n : ℕ), ∫⁻ (a : α), g n a ∂μ.withDensity f = ∫⁻ (a : α), (f * g n) a ∂μ
m n : ℕ
hmn : m ≤ n
x : α
⊢ f x * g m x ≤ f x * g n x

Tactic:
grw [h_mono_g hmn x]

Goal state after:
Module: Mathlib.Algebra.QuadraticDiscriminant

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

Tactic:
refine lt_of_le_of_ne (discrim_le_zero this) fun h' ↦ ?_

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
h' : discrim a b c = 0
⊢ False
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ √x * (√y)⁻¹ = √x / √y

Tactic:
division_def

Goal state after:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ √x * (√y)⁻¹ = √x * (√y)⁻¹
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ √x * (√y)⁻¹ = √x / √y

Tactic:
division_def

Goal state after:
x y : ℝ
hy : 0 ≤ y
⊢ √x * (√y)⁻¹ = √x * (√y)⁻¹
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: n : ℕ
⊢ ↑‖↑n‖₊ = ↑↑n

Tactic:
by simp [norm_natCast]

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

Goal state before:
pp: z : ℂ
hz : z = 0
⊢ |z.re / ‖z‖| ≤ 1

Tactic:
simp [hz, zero_le_one]

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

Goal state before:
pp: z : ℂ
hz : z = 0
⊢ |z.im / ‖z‖| ≤ 1

Tactic:
simp [hz, zero_le_one]

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

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
i : ℕ
H : ∀ j ≥ i, ‖↑f j - ↑f i‖ < ε
j : ℕ
ij : j ≥ i
⊢ |(fun n ↦ (↑f n).im) j - (fun n ↦ (↑f n).im) i| < ε

Tactic:
by
    simpa only [← ofReal_sub, norm_real, sub_re, sub_im] using (abs_im_le_norm _).trans_lt <| H _ ij

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

Goal state before:
pp: case «0».«0»
⊢ (LinearMap.toMatrix basisOneI basisOneI) (↑↑conjAe) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![1, 0; 0, -1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [LinearMap.toMatrix_apply]

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

Goal state before:
pp: case «0».«1»
⊢ (LinearMap.toMatrix basisOneI basisOneI) (↑↑conjAe) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![1, 0; 0, -1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [LinearMap.toMatrix_apply]

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

Goal state before:
pp: case «1».«0»
⊢ (LinearMap.toMatrix basisOneI basisOneI) (↑↑conjAe) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![1, 0; 0, -1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [LinearMap.toMatrix_apply]

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

Goal state before:
pp: case «1».«1»
⊢ (LinearMap.toMatrix basisOneI basisOneI) (↑↑conjAe) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![1, 0; 0, -1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [LinearMap.toMatrix_apply]

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

Goal state before:
pp: z w : ℂ
⊢ dist ((starRingEnd ℂ) z) w = dist z ((starRingEnd ℂ) w)

Tactic:
rw [← dist_conj_conj, conj_conj]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 < z ↔ ∃ x > 0, ↑x = z

Tactic:
by
  simp_rw [pos_iff (K := K), ext_iff (K := K)]; aesop

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
f' : α → E'
l : Filter α
g : α → ℝ
h : (fun x ↦ ‖f' x‖) =ᶠ[l] g
x : α
hx : (fun x ↦ ‖f' x‖) x = g x
⊢ (fun x ↦ ‖f' x‖) x = (fun x ↦ ‖g x‖) x

Tactic:
simp only [← hx, norm_norm]

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hgk : g =o[l] k
hc : 0 < c
⊢ f =o[l] k

Tactic:
by
  simp only [IsLittleO_def] at *
  intro c' c'pos
  have : 0 < c' / c := div_pos c'pos hc
  exact (hfg.trans (hgk this) hc.le).congr_const (mul_div_cancel₀ _ hc.ne')

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

Goal state before:
pp: case cons
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
i : ι
L : List ι
ihL :
  (∀ i ∈ L, f i =O[l] g i) →
    (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) L).prod) =O[l] fun x ↦ (List.map (fun x_1 ↦ g x_1 x) L).prod
hf : ∀ i_1 ∈ i :: L, f i_1 =O[l] g i_1
⊢ (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) (i :: L)).prod) =O[l] fun x ↦ (List.map (fun x_1 ↦ g x_1 x) (i :: L)).prod

Tactic:
| cons i L ihL =>

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

Goal state before:
pp: case cons
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
f : ι → α → R
g : ι → α → 𝕜
i : ι
L : List ι
ihL :
  (∀ i ∈ L, f i =O[l] g i) →
    (∃ i ∈ L, f i =o[l] g i) →
      (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) L).prod) =o[l] fun x ↦ (List.map (fun x_1 ↦ g x_1 x) L).prod
h₁ : ∀ i_1 ∈ i :: L, f i_1 =O[l] g i_1
h₂ : ∃ i_1 ∈ i :: L, f i_1 =o[l] g i_1
⊢ (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) (i :: L)).prod) =o[l] fun x ↦ (List.map (fun x_1 ↦ g x_1 x) (i :: L)).prod

Tactic:
| cons i L ihL =>

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

Goal state before:
pp: x : ℂ
⊢ sinh (3 * x) = 4 * sinh x ^ 3 + 3 * sinh x

Tactic:
have h1 : x + 2 * x = 3 * x := by ring
  rw [← h1, sinh_add x (2 * x)]
  simp only [cosh_two_mul, sinh_two_mul]
  have h2 : cosh x * (2 * sinh x * cosh x) = 2 * sinh x * cosh x ^ 2 := by ring
  rw [h2, cosh_sq]
  ring

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

Goal state before:
pp: x : ℂ
⊢ sinh (3 * x) = 4 * sinh x ^ 3 + 3 * sinh x

Tactic:
by
  have h1 : x + 2 * x = 3 * x := by ring
  rw [← h1, sinh_add x (2 * x)]
  simp only [cosh_two_mul, sinh_two_mul]
  have h2 : cosh x * (2 * sinh x * cosh x) = 2 * sinh x * cosh x ^ 2 := by ring
  rw [h2, cosh_sq]
  ring

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

Goal state before:
pp: x : ℂ
⊢ sinh (x * I) / cosh (x * I) = tan x * I

Tactic:
cosh_mul_I,

Goal state after:
x : ℂ
⊢ sinh (x * I) / cos x = tan x * I
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ sinh x / cosh x * I = tanh x * I

Tactic:
tanh_eq_sinh_div_cosh

Goal state after:
x : ℂ
⊢ sinh x / cosh x * I = sinh x / cosh x * I
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
cosh_mul_I,

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

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

Tactic:
cosh_mul_I,

Goal state after:
x y : ℂ
⊢ cos x * cos y + sinh (x * I) * sinh (y * I) = cos x * cos y - sin x * sin y
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ (cos ↑x).im = 0

Tactic:
rw [← ofReal_cos_ofReal_re, ofReal_im]

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

Goal state before:
pp: x : ℂ
⊢ sin x ^ 2 + cos x ^ 2 = cosh (x * I) ^ 2 - sinh (x * I) ^ 2

Tactic:
cosh_mul_I,

Goal state after:
x : ℂ
⊢ sin x ^ 2 + cos x ^ 2 = cos x ^ 2 - sinh (x * I) ^ 2
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / ↑m.factorial‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / ↑m.factorial‖ / 2 ≤
    ‖-x * I‖ ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹) / 2 +
      ‖x * I‖ ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹) / 2

Tactic:
by
      grw [exp_bound (by simpa) (by simp), exp_bound (by simpa) (by simp)]

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

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖cexp (-x * I) - ∑ m ∈ range 5, (-x * I) ^ m / ↑m.factorial‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 5, (x * I) ^ m / ↑m.factorial‖ / 2 ≤
    ‖-x * I‖ ^ 5 * (↑(Nat.succ 5) * (↑(Nat.factorial 5) * ↑5)⁻¹) / 2 +
      ‖x * I‖ ^ 5 * (↑(Nat.succ 5) * (↑(Nat.factorial 5) * ↑5)⁻¹) / 2

Tactic:
by
      grw [exp_bound (by simpa) (by simp), exp_bound (by simpa) (by simp)]

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

Goal state before:
pp: x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : |x| = x
⊢ rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n + 1) / (↑n.factorial * ↑n)

Tactic:
have h4 : |x| ≤ 1 := by rwa [h3]

Goal state after:
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : |x| = x
h4 : |x| ≤ 1
⊢ rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n + 1) / (↑n.factorial * ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: a : ℝ
⊢ UniformContinuousOn cexp {x | x.re ≤ a}

Tactic:
have : Continuous (cexp - 1) := Continuous.sub (by fun_prop) continuous_one
  rw [Metric.uniformContinuousOn_iff, Metric.continuous_iff'] at *
  intro ε hε
  simp only [gt_iff_lt, Pi.sub_apply, Pi.one_apply, dist_sub_eq_dist_add_right,
    sub_add_cancel] at this
  have ha : 0 < ε / (2 * Real.exp a) := by positivity
  have H := this 0 (ε / (2 * Real.exp a)) ha
  rw [Metric.eventually_nhds_iff] at H
  obtain ⟨δ, hδ⟩ := H
  refine ⟨δ, hδ.1, ?_⟩
  intro x _ y hy hxy
  have h3 := hδ.2 (y := x - y) (by simpa only [dist_eq_norm, sub_zero] using hxy)
  rw [dist_eq_norm, exp_zero] at *
  have : cexp x - cexp y = cexp y * (cexp (x - y) - 1) := by
    rw [mul_sub_one, ← exp_add]
    ring_nf
  rw [this, mul_comm]
  have hya : ‖cexp y‖ ≤ Real.exp a := by simpa only [norm_exp, Real.exp_le_exp]
  simp only [gt_iff_lt, dist_zero_right, Set.mem_ofPred_eq, norm_mul, Complex.norm_exp] at *
  apply lt_of_le_of_lt (mul_le_mul h3.le hya (Real.exp_nonneg y.re) ha.le)
  simp [field]

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:
simp only [isBigO_one_iff, norm_eq_abs, abs_exp, isBoundedUnder_le_exp_comp]

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
x : E
s : Set E
⊢ infEDist x⁻¹ ((fun x ↦ x⁻¹) '' s) = infEDist x s

Tactic:
infEDist_image isometry_inv

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
x : E
s : Set E
⊢ infEDist x s = infEDist x s
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ s * closedBall 1 δ = cthickening δ s

Tactic:
rw [hs.cthickening_eq_biUnion_closedBall hδ]
  ext x
  simp only [mem_mul, dist_eq_norm_div, exists_prop, mem_iUnion, mem_closedBall,
    ← eq_div_iff_mul_eq'', div_one, exists_eq_right]

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
⊢ Summable fun n ↦ ‖↑(u n) * r ^ n‖

Tactic:
← norm_norm

Goal state after:
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
⊢ Summable fun n ↦ ‖↑(u n) * r ^ n‖
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
⊢ Summable fun n ↦ ‖↑(u n) * r ^ n‖

Tactic:
rw [← norm_norm] at hrr'

Goal state after:
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
⊢ Summable fun n ↦ ‖↑(u n) * r ^ n‖
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x z : E
hz : z ∈ s
hxz : dist x z < δ + ε
⊢ ∃ z, (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε

Tactic:
obtain ⟨y, hxy, hyz⟩ := exists_dist_lt_lt hε hδ hxz

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x z : E
hz : z ∈ s
hxz : dist x z < δ + ε
y : E
hxy : dist x y < ε
hyz : dist y z < δ
⊢ ∃ z, (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ Function.Antiperiodic sinh (↑π * I)

Tactic:
by
  simp [Complex.sinh_add, sinh_mul_I, cosh_mul_I]

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ↑(σ t) ≤ 1 / 2
h : 1 - ↑t ≤ 1 / 2
h₁ : ↑t ≤ 1 / 2
ht : ↑t = 1 / 2
⊢ γ ⟨2 * ↑(σ t), ⋯⟩ = γ' (σ ⟨2 * ↑t, ⋯⟩)

Tactic:
norm_num [ht]

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

Goal state before:
pp: p : ℝ
hp : p ≠ 0
x✝ : AddCircle p
ε : ℝ
hε : |p| / 2 ≤ ε
x : AddCircle p
⊢ x ∈ closedBall x✝ ε

Tactic:
simpa only [mem_closedBall, dist_eq_norm] using (norm_le_half_period p hp).trans hε

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: case pos
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : t₀ ≤ ↑0
h₂ : ¬↑0 ≤ t₁
h₄✝ : t₀ ≤ t₁
h₄ : t₁ ≤ 0
⊢ γ.extend t₁ = γ.extend t₀

Tactic:
simp [γ.extend_of_le_zero h₄, γ.extend_of_le_zero h₁]

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

Goal state before:
pp: case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
rw [arccos_eq_pi_div_two_sub_arcsin, sin_pi_div_two_sub, cos_arcsin]

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

Goal state before:
pp: case neg.mp
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π → z.re < 0 ∧ z.im = 0

pp: case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re < 0 ∧ z.im = 0 → z.arg = π

Tactic:
· intro h
    rw [← norm_mul_cos_add_sin_mul_I z, h]
    simp [h₀]

Goal state after:
case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re < 0 ∧ z.im = 0 → z.arg = π
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
← log_one

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