mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case h₁
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := ⋯
hu : u.Countable
t' : Set α := ⋯
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ MeasurableSet (g '' (t \ t'))

Tactic:
apply (ht.diff ht').image_of_continuousOn_injOn (h'g.mono sdiff_subset)

Goal state after:
case h₁
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := ⋯
hu : u.Countable
t' : Set α := ⋯
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ InjOn g (t \ t')
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
H✝ : Type u_2
inst✝⁹ : MeasurableSpace G
inst✝⁸ : MeasurableSpace H✝
inst✝⁷ : Mul G
μ : Measure G
inst✝⁶ : MeasurableMul G
inst✝⁵ : μ.IsMulRightInvariant
inst✝⁴ : SFinite μ
H : Type u_3
inst✝³ : Mul H
mH : MeasurableSpace H
ν : Measure H
inst✝² : MeasurableMul H
inst✝¹ : ν.IsMulRightInvariant
inst✝ : SFinite ν
⊢ (μ.prod ν).IsMulRightInvariant

Tactic:
constructor
  rintro ⟨g, h⟩
  change map (Prod.map (· * g) (· * h)) (μ.prod ν) = μ.prod ν
  rw [← map_prod_map _ _ (measurable_mul_const g) (measurable_mul_const h),
    map_mul_right_eq_self μ g, map_mul_right_eq_self ν h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : SFinite ν
ρ : Measure (α × β)
inst✝ : SFinite ρ
⊢ SFinite ρ.snd

Tactic:
rw [snd]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : SFinite ν
ρ : Measure (α × β)
inst✝ : SFinite ρ
⊢ SFinite (map Prod.snd ρ)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : SFinite ν
ρ : Measure (α × β)
inst✝ : IsFiniteMeasure ρ
⊢ IsFiniteMeasure ρ.snd

Tactic:
rw [snd]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : SFinite ν
ρ : Measure (α × β)
inst✝ : IsFiniteMeasure ρ
⊢ IsFiniteMeasure (map Prod.snd ρ)
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
s : Set G
x✝ : MeasurableSet s
⊢ μ s⁻¹ = 0 → μ s = 0

Tactic:
measure_inv_null,

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
s : Set G
x✝ : MeasurableSet s
⊢ μ s = 0 → μ s = 0
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : CommGroup G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : μ.IsInvInvariant
f g : G → ℝ≥0∞
x : G
⊢ ∫⁻ (x_1 : G), f (x * x_1⁻¹) * g ((x * x_1⁻¹)⁻¹ * x) ∂μ = ∫⁻ (y : G), g y * f (y⁻¹ * x) ∂μ

Tactic:
simp [mul_comm]

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
⊢ ∫⁻ (a : α) in s, (f + g) a ∂μ = (μ.withDensity f + μ.withDensity g) s

Tactic:
Measure.add_apply,

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 ∂μ = (μ.withDensity f) s + (μ.withDensity g) s
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: 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)
n : ℕ
IH : μ (L n) = ↑(n + 1) * μ K
⊢ μ (L n) + μ (g (L n) • K) = ↑(n + 1 + 1) * μ K

Tactic:
by
          simp only [IH, measure_smul, add_mul, Nat.cast_add, Nat.cast_one, one_mul]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : c = 0
⊢ (c • μ).InnerRegularCompactLTTop

Tactic:
simp only [hc, zero_smul]
    infer_instance

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun x ↦ ↑(f x) * g x) =ᵐ[μ] g'
a : α
hfga : ↑(f a) * g a = g' a
hff'a : f a = f' a
h'a : ↑(f a) ≠ 0
⊢ g a = (↑(f' a))⁻¹ * g' a

Tactic:
rw [hff'a] at hfga h'a

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : (fun x ↦ ↑(f x) * g x) =ᵐ[μ] g'
a : α
hfga : ↑(f' a) * g a = g' a
hff'a : f a = f' a
h'a : ↑(f' a) ≠ 0
⊢ g a = (↑(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
⊢ QuasiMeasurePreserving (fun h ↦ h * g) μ μ

Tactic:
by
  refine ⟨measurable_mul_const g, AbsolutelyContinuous.mk fun s hs => ?_⟩
  rw [map_apply (measurable_mul_const g) hs, measure_mul_right_null]; exact id

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
h : 0 ≤ᵐ[μ] f
⊢ HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ∞

Tactic:
by
  rw [hasFiniteIntegral_iff_enorm, lintegral_enorm_of_ae_nonneg h]

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

Goal state before:

Tactic:
∫⁻ a, g a ∂μ.withDensity f' = ∫⁻ a, g' a ∂μ.withDensity f' := lintegral_congr_ae hg.ae_eq_mk
    _ = ∫⁻ a, (f' * g') a ∂μ :=
      (lintegral_withDensity_eq_lintegral_mul _ hf.measurable_mk hg.measurable_mk)
    _ = ∫⁻ a, (f' * g) a ∂μ := by
      apply lintegral_congr_ae
      apply ae_of_ae_restrict_of_ae_restrict_compl { x | f' x ≠ 0 }
      · have Z := hg.ae_eq_mk
        rw [EventuallyEq, ae_withDensity_iff_ae_restrict hf.measurable_mk] at Z
        filter_upwards [Z]
        intro x hx
        simp only [g', hx, Pi.mul_apply]
      · have M : MeasurableSet { x : α | f' x ≠ 0 }ᶜ :=
          (hf.measurable_mk (measurableSet_singleton 0).compl).compl
        filter_upwards [ae_restrict_mem M]
        intro x hx
        simp only [Classical.not_not, mem_ofPred_eq, mem_compl_iff] at hx
        simp only [hx, zero_mul, Pi.mul_apply]
    _ = ∫⁻ a : α, (f * g) a ∂μ := by
      apply lintegral_congr_ae
      filter_upwards [hf.ae_eq_mk]
      intro x hx
      simp only [f', hx, Pi.mul_apply]

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

Goal state before:
pp: z w : ℂ
⊢ normSq z + normSq w + 2 * (z * (starRingEnd ℂ) w).re ≤ normSq z + normSq w + 2 * (√(normSq z) * √(normSq w))

Tactic:
← Real.sqrt_mul <| normSq_nonneg z,

Goal state after:
z w : ℂ
⊢ normSq z + normSq w + 2 * (z * (starRingEnd ℂ) w).re ≤ normSq z + normSq w + 2 * √(normSq z * normSq w)
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: n : ℤ
⊢ ‖↑n‖ = |↑n|

Tactic:
rw [← ofReal_intCast, norm_real, Real.norm_eq_abs]

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

Goal state before:
pp: z : ℂ
⊢ ‖z‖ ≤ √2 * max |z.re| |z.im|

Tactic:
obtain ⟨x, y⟩ := z

Goal state after:
x y : ℝ
⊢ ‖{ re := x, im := y }‖ ≤ √2 * max |{ re := x, im := y }.re| |{ re := x, im := y }.im|
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ ((μ.withDensity f).withDensity fun x ↦ (f x)⁻¹) = μ

Tactic:
rw [← withDensity_mul₀ hf hf.fun_inv]
  suffices (f * fun x ↦ (f x)⁻¹) =ᵐ[μ] 1 by
    rw [withDensity_congr_ae this, withDensity_one]
  filter_upwards [hf_ne_zero, hf_ne_top] with x hf_ne_zero hf_ne_top
  simp only [Pi.mul_apply]
  rw [ENNReal.mul_inv_cancel hf_ne_zero hf_ne_top, Pi.one_apply]

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

Goal state before:
pp: α : Type u_1
q : ℚ
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
ext <;> simp [Rat.cast_def, div_re, div_im, mul_div_mul_comm]

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

Goal state before:
pp: case refine_2
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : f.SurjectiveOnWith K C
⊢ f.SurjectiveOnWith K (|C| + 1)

Tactic:
apply h.mono

Goal state after:
case refine_2
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : f.SurjectiveOnWith K C
⊢ C ≤ |C| + 1
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: case refine_2
V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f : NormedAddGroupHom V W
h : ‖f‖ ≤ 1
v : V
⊢ ‖f v‖ ≤ ‖v‖

Tactic:
simpa using le_of_opNorm_le f h v

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

Goal state before:
pp: E : Type u_2
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CStarRing E
inst✝ : Nontrivial E
U : ↥(unitary E)
⊢ ‖↑U‖ = 1

Tactic:
rw [← sq_eq_sq₀ (norm_nonneg _) zero_le_one, one_pow 2, sq, ← CStarRing.norm_star_mul_self,
    Unitary.coe_star_mul_self, CStarRing.norm_one]

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

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

Tactic:
← dist_conj_conj,

Goal state after:
z w : ℂ
⊢ dist ((starRingEnd ℂ) ((starRingEnd ℂ) z)) ((starRingEnd ℂ) w) = dist z ((starRingEnd ℂ) w)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ ↑(-im z) = -(I * ((starRingEnd K) z - z) / 2)

Tactic:
← I_mul_re,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ ↑(re (I * z)) = -(I * ((starRingEnd K) z - z) / 2)
Module: Mathlib.Topology.OpenPartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ IsOpen[inst✝] (range (e.source.domRestrict ↑e))

Tactic:
range_domRestrict,

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ IsOpen[inst✝] (↑e '' e.source)
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
⊢ ∀ (z : 𝕜),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          im)
        ((starRingEnd 𝕜) z) =
      -(⋯ ▸
            let __spread.0 := h.toNormedField;
            im)
          z

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

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
x : α
hx₁ : ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
hx₂ : ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
⊢ max c₁ c₂ * ‖g₁ x‖ + max c₁ c₂ * ‖g₂ x‖ = max c₁ c₂ * ‖‖g₁ x‖ + ‖g₂ x‖‖

Tactic:
by
        rw [Real.norm_of_nonneg (add_nonneg (norm_nonneg _) (norm_nonneg _)), mul_add]

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

Goal state before:
pp: case mpr
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
⊢ (∃ b, 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖) → (fun _x ↦ c) =O[l] f'

Tactic:
rintro ⟨b, hb₀, hb⟩

Goal state after:
case mpr
α : Type u_1
E' : Type u_6
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
b : ℝ
hb₀ : 0 < b
hb : ∀ᶠ (x : α) in l, b ≤ ‖f' x‖
⊢ (fun _x ↦ c) =O[l] f'
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
C : ℝ
i : α → Finset ι
hAB : ∀ᶠ (x : ι × α) in ⊤ ×ˢ l, ‖Function.uncurry A x‖ ≤ C * ‖Function.uncurry B x‖
s₁ : ι → Prop
hs₁ : ∀ᶠ (x : ι) in ⊤, s₁ x
s₂ : α → Prop
hs₂ : ∀ᶠ (y : α) in l, s₂ y
hbound : ∀ {x : ι}, s₁ x → ∀ {y : α}, s₂ y → ‖Function.uncurry A (x, y)‖ ≤ C * ‖Function.uncurry B (x, y)‖
H : α
hH : s₂ H
⊢ ‖∑ j ∈ i H, A j H‖ ≤ C * ‖∑ j ∈ i H, ‖B j H‖‖

Tactic:
calc
    ‖∑ j ∈ i H, A j H‖ ≤ ∑ j ∈ i H, ‖A j H‖ := norm_sum_le ..
    _ ≤ ∑ j ∈ i H, C * ‖B j H‖ :=
        Finset.sum_le_sum fun j _ => hbound (Filter.eventually_top.mp hs₁ j) hH
    _ = C * ∑ j ∈ i H, ‖B j H‖ := (Finset.mul_sum ..).symm
    _ = C * ‖∑ j ∈ i H, ‖B j H‖‖ := by
        congr; rw [Real.norm_of_nonneg (Finset.sum_nonneg (fun _ _ ↦ norm_nonneg _))]

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

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

Tactic:
← cosh_mul_I,

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

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

Tactic:
← cosh_mul_I,

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

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

Tactic:
← cosh_mul_I,

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

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

Tactic:
← cosh_mul_I,

Goal state after:
x : ℂ
⊢ cosh ((starRingEnd ℂ) x * I) = (starRingEnd ℂ) (cos x)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cosh ((starRingEnd ℂ) (x * -I)) = (starRingEnd ℂ) (cos x)

Tactic:
← cosh_mul_I,

Goal state after:
x : ℂ
⊢ cosh ((starRingEnd ℂ) (x * -I)) = (starRingEnd ℂ) (cosh (x * I))
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 : ℕ), g x = 0 → f x = 0
⊢ f =O[cofinite] g ↔ ∃ C, ∀ (x : ℕ), ‖f x‖ ≤ C * ‖g x‖

Tactic:
isBigO_cofinite_iff h

Goal state after:
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h : ∀ (x : ℕ), g x = 0 → f x = 0
⊢ (∃ C, ∀ (x : ℕ), ‖f x‖ ≤ C * ‖g x‖) ↔ ∃ C, ∀ (x : ℕ), ‖f x‖ ≤ C * ‖g x‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cos (3 * x) = 4 * cos x ^ 3 - 3 * cos x

Tactic:
← cosh_mul_I,

Goal state after:
x : ℂ
⊢ cosh (3 * x * I) = 4 * cos x ^ 3 - 3 * cos x
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
by
  simp [exp_mul_I]

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

Goal state before:
pp: case neg
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
hfg : f =O[atTop] g
l : Filter ℕ
h✝ : ∀ᶠ (n : ℕ) in l, g n = 0 → f n = 0
C : ℝ
hC_pos : C > 0
hC : ∀ ⦃x : ℕ⦄, g x ≠ 0 → ‖f x‖ ≤ C * ‖g x‖
x : ℕ
h : g x = 0 → f x = 0
hf : ¬f x = 0
⊢ ‖f x‖ ≤ C * ‖g x‖

Tactic:
exact hC fun a ↦ hf (h a)

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

Goal state before:
pp: α : Type u_1
F' : Type u_7
inst✝² : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst✝¹ : Fintype ι
E' : ι → Type u_18
inst✝ : (i : ι) → SeminormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
⊢ f =o[l] g' ↔ ∀ (i : ι), (fun x ↦ f x i) =o[l] g'

Tactic:
simp +contextual only [IsLittleO_def, isBigOWith_pi, le_of_lt]
  exact ⟨fun h i c hc => h hc i, fun h c hc i => h i hc⟩

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

Goal state before:
pp: x : ℝ
⊢ sin x ^ 2 = 1 / 2 - cos (2 * x) / 2

Tactic:
by
  rw [sin_sq, cos_sq, ← sub_sub, sub_half]

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
ha : a < 0
k : ℤ
⊢ a ^ (2 * k + 1) < 0

Tactic:
zpow_add_one₀ ha.ne

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
ha : a < 0
k : ℤ
⊢ a ^ (2 * k) * a < 0
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : OpenPartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
C : ℝ
h : IsBigOWith C (𝓝 b) f g
⊢ Tendsto (↑e) (𝓝 (↑e.symm b)) (𝓝 b)

Tactic:
by
      have := e.continuousAt (e.map_target hb)
      rwa [ContinuousAt, e.rightInvOn hb] at this

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
c : F
inst✝¹ : SeminormedAddGroup E
inst✝ : Norm F
hf : ContinuousOn f s
hs : IsCompact s
hc : ‖c‖ ≠ 0
⊢ IsBigOWith (sSup (Norm.norm '' f '' s) / ‖c‖) (𝓟 s) f fun x ↦ c

Tactic:
by
  rw [isBigOWith_principal, div_mul_cancel₀ _ hc]
  exact fun x hx ↦ hs.image_of_continuousOn hf |>.image continuous_norm
   |>.isLUB_sSup (Set.image_nonempty.mpr <| Set.image_nonempty.mpr ⟨x, hx⟩)
   |>.left <| Set.mem_image_of_mem _ <| Set.mem_image_of_mem _ hx

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 n.succ) ≤ abv (f n.succ) * r ^ n.succ * r⁻¹ ^ n.succ

Tactic:
inv_pow _ _,

Goal state after:
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 n.succ) ≤ abv (f n.succ) * r ^ n.succ * (r ^ n.succ)⁻¹
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
ε : ℝ
x : M
⊢ ↑x ∈ mk '' ball 1 ε ↔ ↑x ∈ {x | ‖x‖ < ε}

Tactic:
rw [ball_one_eq, mem_ofPred_eq, norm_lt_iff, mem_image]

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
ε : ℝ
x : M
⊢ (∃ x_1 ∈ {x | ‖x‖ < ε}, ↑x_1 = ↑x) ↔ ∃ m, ↑m = ↑x ∧ ‖m‖ < ε
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
x : M
⊢ x ∈ S.normedMk.ker.topologicalClosure

Tactic:
rw [S.ker_normedMk, ← SetLike.mem_coe, h]

Goal state after:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure = univ
x : M
⊢ x ∈ univ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x y : ℝ
h : x ≤ y
n : ℕ
⊢ x.sqrtTwoAddSeries (n + 1) ≤ y.sqrtTwoAddSeries (n + 1)

Tactic:
rw [sqrtTwoAddSeries, sqrtTwoAddSeries]

Goal state after:
x y : ℝ
h : x ≤ y
n : ℕ
⊢ √(2 + x.sqrtTwoAddSeries n) ≤ √(2 + y.sqrtTwoAddSeries n)
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ frontier (closedBall x r) = sphere x r

Tactic:
by
  rw [frontier, closure_closedBall, interior_closedBall' x r, closedBall_sdiff_ball]

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: ⊢ sin (π / 3) = √3 / 2

Tactic:
by
  rw [← cos_pi_div_two_sub, ← cos_pi_div_six]
  congr
  ring

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

Goal state before:
pp: case pos
R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n ↦ x ^ n
⊢ ‖∑' (n : ℕ), x ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Tactic:
hx.tsum_eq_zero_add

Goal state after:
case pos
R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n ↦ x ^ n
⊢ ‖x ^ 0 + ∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
hε' : 0 < ε
hεδ : 0 < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε ≤ ε

Tactic:
rw [← div_le_one hεδ] at h

Goal state after:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z / (ε + δ) ≤ 1
hε' : 0 < ε
hεδ : 0 < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε ≤ ε
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inr.top
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
h : edist x z < ∞
⊢ infEDist x (thickening δ s) + ENNReal.ofReal δ < ∞

Tactic:
exact add_lt_top.2 ⟨lt_top_iff_ne_top.2 <| infEDist_ne_top ⟨z, self_subset_thickening hδ _ hz⟩,
      ofReal_lt_top⟩

Goal state after: