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

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : MeasurableConstSMul G α
tfae_1_iff_2 : SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → μ ((fun x ↦ c • x) ⁻¹' s) = μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), Measure.map (fun x ↦ c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), Measure.map (fun x ↦ c • x) μ = μ) → ∀ (c : G), MeasurePreserving (fun x ↦ c • x) μ μ
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving (fun x ↦ c • x) μ μ) → ∀ (c : G) (s : Set α), μ ((fun x ↦ c • x) ⁻¹' s) = μ s
H : ∀ (c : G) (s : Set α), μ ((fun x ↦ c • x) ⁻¹' s) = μ s
c : G
s : Set α
⊢ μ (c • s) = μ s

Tactic:
rw [← preimage_smul_inv]
    apply H

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

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

Tactic:
exact measure_mono <| subset_inter (subset_toMeasurable μ (s ∩ A)) inter_subset_left

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

Goal state before:
pp: case compl
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
s : Set α
hs : MeasurableSet s
H : ∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ s, ∃ U ⊇ s, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ s ≤ μ F + ε ∧ μ U ≤ μ s + ε
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ F ⊆ sᶜ, ∃ U ⊇ sᶜ, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ sᶜ ≤ μ F + ε ∧ μ U ≤ μ sᶜ + ε

Tactic:
rcases H ε hε with ⟨F, hFs, U, hsU, hFc, hUo, hF, hU⟩

Goal state after:
case compl
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
s : Set α
hs : MeasurableSet s
H : ∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ s, ∃ U ⊇ s, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ s ≤ μ F + ε ∧ μ U ≤ μ s + ε
ε : ℝ≥0∞
hε : ε ≠ 0
F : Set α
hFs : F ⊆ s
U : Set α
hsU : U ⊇ s
hFc : IsClosed[inst✝²] F
hUo : IsOpen[inst✝²] U
hF : μ s ≤ μ F + ε
hU : μ U ≤ μ s + ε
⊢ ∃ F ⊆ sᶜ, ∃ U ⊇ sᶜ, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ sᶜ ≤ μ F + ε ∧ μ U ≤ μ 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
inst✝² : LocallyCompactSpace G
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : μ.InnerRegularCompactLTTop
k : Set G
hk : IsCompact k
h'k : IsClosed[inst✝⁶] k
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set G
hUk : k ⊆ U
hU : IsOpen[inst✝⁶] U
hμUk : μ U < μ k + ε
V : Set G
hV1 : V ∈ 𝓝 1
hVkU : V * k ⊆ U
g : G
hg : g ∈ V
⊢ μ (g • k \ k) ≤ μ (U \ k)

Tactic:
by
      gcongr
      exact (smul_set_subset_smul hg).trans hVkU

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
⊢ (map (⇑f) μ).InnerRegular ↔ μ.InnerRegular

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.map f⟩
  convert! h.map f.symm
  rw [map_map f.symm.continuous.measurable f.continuous.measurable]
  simp

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
⊢ EventuallyConst s (ae μ)⁻¹ ↔ EventuallyConst s (ae μ)

Tactic:
inv_ae

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
⊢ EventuallyConst s (ae μ) ↔ EventuallyConst s (ae μ)
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s + ν s
h : μ s ≠ 0
h' : ν s ≠ 0
u : ℝ≥0∞
hu : u < μ s
v : ℝ≥0∞
hv : v < ν s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < μ K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < ν K'
⊢ u + v ≤ (μ + ν) (K ∪ K')

Tactic:
apply (add_le_add h'K.le h'K'.le).trans

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s + ν s
h : μ s ≠ 0
h' : ν s ≠ 0
u : ℝ≥0∞
hu : u < μ s
v : ℝ≥0∞
hv : v < ν s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < μ K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < ν K'
⊢ μ K + ν K' ≤ (μ + ν) (K ∪ K')
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, IsOpen[inst✝⁴] U ∧ μ U < ∞ ∧ μ (U ∆ s) < ε

Tactic:
refine ⟨U, hUo, hμU.trans_le le_top, ?_⟩

Goal state after:
α : 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 ∆ s) < ε
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α ≃ₜ β
⊢ (map (⇑f) μ).Regular ↔ μ.Regular

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.map f⟩
  convert! h.map f.symm
  rw [map_map f.symm.continuous.measurable f.continuous.measurable]
  simp

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

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
t s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
hs : MeasurableSet s
⊢ μ' s * ν' t = ν' s * μ' t

Tactic:
wlog ht : MeasurableSet t generalizing t

Goal state after:
case inr
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
t s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
hs : MeasurableSet s
this : ∀ (t : Set G), MeasurableSet t → μ' s * ν' t = ν' s * μ' t
ht : ¬MeasurableSet t
⊢ μ' s * ν' t = ν' s * μ' t

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
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)
⊢ Measurable fun b ↦ μ.withDensity (f b)

Tactic:
rw [Measure.measurable_measure]
  intro s hs
  simp only [withDensity_apply _ hs]
  fun_prop

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:
hasFiniteIntegral_iff_enorm,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
h : 0 ≤ᵐ[μ] f
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞ ↔ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ∞
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

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

Tactic:
hasFiniteIntegral_iff_enorm,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
⊢ ∫⁻ (a : α), ‖(f a).toReal‖ₑ ∂μ < ∞
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ ∀ (a b c : ℂ), a + b + c = a + (b + c)

Tactic:
by intros; ext <;> simp <;> ring

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

Goal state before:
pp: ⊢ ∀ (a b : ℂ), a + b = b + a

Tactic:
by intros; ext <;> simp <;> ring

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

Goal state before:
pp: x y : ℝ
⊢ ↑x < ↑y ↔ x < y

Tactic:
by simp [lt_def, ofReal]

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

Goal state before:
pp: ⊢ ∀ (a b c : ℂ), a * b * c = a * (b * c)

Tactic:
by intros; ext <;> simp <;> ring

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

Goal state before:
pp: ⊢ ∀ (a b : ℂ), a * b = b * a

Tactic:
by intros; ext <;> simp <;> ring

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

Goal state before:
pp: z : ℂ
x✝ : ∃ r, z = ↑r
h : ℝ
e : z = ↑h
⊢ (starRingEnd ℂ) ↑h = ↑h

Tactic:
conj_ofReal

Goal state after:
z : ℂ
x✝ : ∃ r, z = ↑r
h : ℝ
e : z = ↑h
⊢ ↑h = ↑h
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ 0⁻¹ = 0

Tactic:
by
  rw [← ofReal_zero, ← ofReal_inv, inv_zero]

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

Goal state before:
pp: z : ℂ
h : z ≠ 0
⊢ z * (starRingEnd ℂ) z * ↑(normSq z)⁻¹ = 1

Tactic:
mul_conj,

Goal state after:
z : ℂ
h : z ≠ 0
⊢ ↑(normSq z) * ↑(normSq z)⁻¹ = 1
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ ‖x * x⋆‖ = ‖x‖ * ‖x‖

Tactic:
← star_star x

Goal state after:
E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ ‖x⋆⋆ * x⋆‖ = ‖x‖ * ‖x‖
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
a b : Rˣ
⊢ ↑a⁻¹ * ↑b ∈ unitary R ↔ a * star a = b * star b

Tactic:
by
  simp [← inv_mul_mem_iff, Units.unitary_eq]

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

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

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

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

Goal state before:
pp: 𝕜 : Type u_2
𝕜' : Type u_3
inst✝¹ : RCLike 𝕜
inst✝ : RCLike 𝕜'
h : RCLike.im RCLike.I = 1
a : 𝕜
⊢ 0 ≤ (RCLike.map 𝕜 𝕜') a ↔ 0 ≤ a

Tactic:
by
  rw [RCLike.nonneg_iff, RCLike.nonneg_iff (K := 𝕜)]
  simp [h]

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

Goal state before:
pp: x : ℂ
hx : 0 ≤ x
⊢ ↑‖x‖ = x

Tactic:
exact RCLike.norm_of_nonneg' hx

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

Goal state before:
pp: case inr
K : Type u_1
inst✝ : RCLike K
z : K
h₀ : z ≠ 0
⊢ z * (starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹ = 1

Tactic:
mul_conj,

Goal state after:
case inr
K : Type u_1
inst✝ : RCLike K
z : K
h₀ : z ≠ 0
⊢ ↑‖z‖ ^ 2 * ↑(‖z‖ ^ 2)⁻¹ = 1
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
n : ℕ
⊢ ‖↑n‖ = ↑n

Tactic:
← ofReal_natCast

Goal state after:
K : Type u_1
inst✝ : RCLike K
n : ℕ
⊢ ‖↑↑n‖ = ↑n
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
⊢ re (x * (starRingEnd K) x) = ‖x * (starRingEnd K) x‖

Tactic:
mul_conj,

Goal state after:
K : Type u_1
inst✝ : RCLike K
x : K
⊢ re (↑‖x‖ ^ 2) = ‖↑‖x‖ ^ 2‖
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z w : K
⊢ z ≤ w ∧ z ≠ w ↔ (re z ≤ re w ∧ re z ≠ re w) ∧ im z = im w

Tactic:
@RCLike.le_iff_re_im K

Goal state after:
K : Type u_1
inst✝ : RCLike K
z w : K
⊢ (re z ≤ re w ∧ im z = im w) ∧ z ≠ w ↔ (re z ≤ re w ∧ re z ≠ re w) ∧ im z = im w
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
h : (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ ↑x * y) a b) ((fun x y ↦ ↑x * y) a c)
⊢ (fun x1 x2 ↦ x1 ≤ x2) b c

Tactic:
obtain ⟨a', ha1, ha2⟩ := pos_iff_exists_ofReal.mp a.2
    rw [← sub_nonneg]
    #adaptation_note /-- 2025-03-29 need beta reduce for https://github.com/leanprover/lean4/issues/7717 -/
    beta_reduce at h
    rw [← ha2, ← sub_nonneg, ← mul_sub, le_iff_lt_or_eq] at h
    rcases h with h | h
    · rw [ofReal_mul_pos_iff] at h
      exact le_of_lt <| h.rec (False.elim <| not_lt_of_gt ·.1 ha1) (·.2)
    · exact ((mul_eq_zero_iff_left <| ofReal_ne_zero.mpr ha1.ne').mp h.symm).ge

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
h : I = 0
x : K
⊢ ↑(re x) = x

Tactic:
nth_rw 2 [← re_add_im x]

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
h : I = 0
x : K
⊢ ↑(re x) = ↑(re x) + ↑(im x) * I
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case e'_1.e'_3
K : Type u_1
inst✝ : RCLike K
z : K
h : im I = 1
this : I ≠ 0
⊢ ‖z‖ = ‖-I * z‖

Tactic:
simp [neg_mul, ← mul_assoc, I_mul_I_of_nonzero this, norm_I_of_ne_zero this]

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

Goal state before:
pp: case e'_1.e'_4
K : Type u_1
inst✝ : RCLike K
z : K
h : im I = 1
this : I ≠ 0
⊢ im z = re (-I * z)

Tactic:
simp [neg_mul, ← mul_assoc, I_mul_I_of_nonzero this, norm_I_of_ne_zero this]

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

Goal state before:
pp: case e'_2
K : Type u_1
inst✝ : RCLike K
z : K
h : im I = 1
this : I ≠ 0
⊢ -I * (I * ↑‖z‖) = ↑‖-I * z‖

Tactic:
simp [neg_mul, ← mul_assoc, I_mul_I_of_nonzero this, norm_I_of_ne_zero this]

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
f' : α → E'
g' : α → F'
l : Filter α
h : f' =Θ[l] g'
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (norm ∘ f') ↔ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (norm ∘ g')

Tactic:
simp only [← isBigO_const_of_ne (one_ne_zero' ℝ), h.isBigO_congr_left]

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

Goal state before:
pp: n : ℕ
pn : NormNum.IsNat n 0
⊢ Multiset.range n = 0

Tactic:
by rw [pn.out, Nat.cast_zero, Multiset.range_zero]

Goal state after:
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 : α → R
g : α → S
h : f =o[l] g
n : ℕ
⊢ (fun x ↦ f x ^ n.succ) =o[l] fun x ↦ g x ^ n.succ

Tactic:
induction n with
  | zero => simpa only [pow_one]
  | succ n ihn => convert! ihn.mul h <;> simp [pow_succ]

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

Goal state before:
pp: x y : ℂ
hj :
  ∀ (j : ℕ),
    ∑ m ∈ range j, (x + y) ^ m / ↑m.factorial =
      ∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial)
⊢ cexp (x + y) = cexp x * cexp y

Tactic:
exp,

Goal state after:
x y : ℂ
hj :
  ∀ (j : ℕ),
    ∑ m ∈ range j, (x + y) ^ m / ↑m.factorial =
      ∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial)
⊢ (exp' (x + y)).lim = (exp' x).lim * (exp' y).lim
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
x✝¹ n : ℕ
x✝ : n ∈ range x✝¹
⊢ (starRingEnd ℂ) x ^ n / ↑↑n.factorial = (starRingEnd ℂ) x ^ n / (starRingEnd ℂ) ↑↑n.factorial

Tactic:
conj_ofReal

Goal state after:
x : ℂ
x✝¹ n : ℕ
x✝ : n ∈ range x✝¹
⊢ (starRingEnd ℂ) x ^ n / ↑↑n.factorial = (starRingEnd ℂ) x ^ n / ↑↑n.factorial
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
⊢ cexp ((starRingEnd ℂ) ↑x) = cexp ↑x

Tactic:
conj_ofReal

Goal state after:
x : ℝ
⊢ cexp ↑x = cexp ↑x
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
h : rexp x = 0
⊢ cexp ↑x = 0

Tactic:
exp,

Goal state after:
x : ℝ
h : (cexp ↑x).re = 0
⊢ cexp ↑x = 0
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ lim ⟨fun n ↦ (↑(exp' ↑x) n).re, ⋯⟩ = rexp x

Tactic:
exp,

Goal state after:
x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ lim ⟨fun n ↦ (↑(exp' ↑x) n).re, ⋯⟩ = (cexp ↑x).re
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ sinh ((starRingEnd ℂ) ↑x) = sinh ↑x

Tactic:
conj_ofReal

Goal state after:
x : ℝ
⊢ sinh ↑x = sinh ↑x
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ cosh ((starRingEnd ℂ) ↑x) = cosh ↑x

Tactic:
conj_ofReal

Goal state after:
x : ℝ
⊢ cosh ↑x = cosh ↑x
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ tanh ((starRingEnd ℂ) ↑x) = tanh ↑x

Tactic:
conj_ofReal

Goal state after:
x : ℝ
⊢ tanh ↑x = tanh ↑x
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E' : Type u_6
𝕜 : Type u_15
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : NormedDivisionRing 𝕜
u : α → E'
v : α → 𝕜
l : Filter α
y : 𝕜
huv : u =o[l] v
hv : Tendsto v l (𝓝 y)
h : u =o[l] fun _x ↦ 1
⊢ Tendsto u l (𝓝 0)

Tactic:
rwa [isLittleO_one_iff] at h

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

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

Tactic:
simp only [cosh_two_mul, sinh_two_mul]

Goal state after:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ cosh x * (cosh x ^ 2 + sinh x ^ 2) + sinh x * (2 * sinh x * cosh x) = 4 * cosh x ^ 3 - 3 * cosh x
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
simp only [cosh_two_mul, sinh_two_mul]

Goal state after:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ sinh x * (cosh x ^ 2 + sinh x ^ 2) + cosh x * (2 * sinh x * cosh x) = 4 * sinh x ^ 3 + 3 * sinh x
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
⊢ ‖cexp x - (const norm (∑ m ∈ range n, x ^ m / ↑m.factorial)).lim‖ ≤ ‖x‖ ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹)

Tactic:
exp,

Goal state after:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
⊢ ‖(exp' x).lim - (const norm (∑ m ∈ range n, x ^ m / ↑m.factorial)).lim‖ ≤ ‖x‖ ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
⊢ ‖cexp x - (const norm (∑ m ∈ range n, x ^ m / ↑m.factorial)).lim‖ ≤ ‖x‖ ^ n / ↑n.factorial * 2

Tactic:
exp,

Goal state after:
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
⊢ ‖(exp' x).lim - (const norm (∑ m ∈ range n, x ^ m / ↑m.factorial)).lim‖ ≤ ‖x‖ ^ n / ↑n.factorial * 2
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ sin ((starRingEnd ℂ) ↑x) = sin ↑x

Tactic:
conj_ofReal

Goal state after:
x : ℝ
⊢ sin ↑x = sin ↑x
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
conj_ofReal

Goal state after:
x : ℝ
⊢ cos ↑x = cos ↑x
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ tan ((starRingEnd ℂ) ↑x) = tan ↑x

Tactic:
conj_ofReal

Goal state after:
x : ℝ
⊢ tan ↑x = tan ↑x
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
conj_ofReal

Goal state after:
x : ℝ
⊢ (↑x).cot = (↑x).cot
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case hbc
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ((‖x‖ / ↑n.succ) ^ k - 1) / (‖x‖ / ↑n.succ - 1) ≤ 2

pp: case hbc.h
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ‖x‖ / ↑n.succ ≠ 1

Tactic:
div_le_iff_of_neg

Goal state after:
case hbc
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ 2 * (‖x‖ / ↑n.succ - 1) ≤ (‖x‖ / ↑n.succ) ^ k - 1

case hbc
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ‖x‖ / ↑n.succ - 1 < 0

case hbc.h
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ‖x‖ / ↑n.succ ≠ 1
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ (Complex.cosh ↑x).re * 2 = rexp x + rexp (-x)

Tactic:
exp,

Goal state after:
x : ℝ
⊢ (Complex.cosh ↑x).re * 2 = (cexp ↑x).re + rexp (-x)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ (Complex.cosh ↑x).re * 2 = (cexp ↑x).re + rexp (-x)

Tactic:
exp,

Goal state after:
x : ℝ
⊢ (Complex.cosh ↑x).re * 2 = (cexp ↑x).re + (cexp ↑(-x)).re
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝¹ : Field α
inst✝ : LinearOrder α
p : ℤ
hp : Even p
a : α
⊢ |a| ^ p = a ^ p

Tactic:
by
  rcases abs_choice a with h | h <;> simp only [h, hp.neg_zpow _]

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

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ x + 1 < rexp x

Tactic:
obtain hx | hx := hx.symm.lt_or_gt
  · exact add_one_lt_exp_of_pos hx
  obtain h' | h' := le_or_gt 1 (-x)
  · linarith [x.exp_pos]
  have hx' : 0 < x + 1 := by linarith
  simpa [add_comm, exp_neg, inv_lt_inv₀ (exp_pos _) hx']
    using exp_bound_div_one_sub_of_interval' (neg_pos.2 hx) h'

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

Goal state before:
pp: case hab
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ 1 - t / ↑n ≤ rexp (-(t / ↑n))

Tactic:
exact one_sub_le_exp_neg _

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

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
⊢ ∃ i, ∀ j ≥ i, |f j - f i| < ε

Tactic:
let ⟨k, hk⟩ := Archimedean.arch a ε0

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
⊢ ∃ i, ∀ j ≥ i, |f j - f i| < ε
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: ⊢ Continuous rexp

Tactic:
unfold Real.exp

Goal state after:
⊢ Continuous fun x ↦ (Complex.exp ↑x).re
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: y : ℝ
h_le : y ≤ rexp (y - 1)
h_mul_le : y * rexp (-y) ≤ rexp (y - 1) * rexp (-y)
⊢ y * rexp (-y) ≤ rexp (-1)

Tactic:
simpa [← exp_add, sub_add_eq_add_sub] using h_mul_le

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

Goal state before:
pp: case mk
M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x✝¹ : M ⧸ S
m : M
r ε : ℝ
x✝ : M ⧸ ⊥
x : M
⊢ ‖quotientBot (Quot.mk (⇑(leftRel ⊥)) x)‖ = ‖Quot.mk (⇑(leftRel ⊥)) x‖

Tactic:
change ‖x‖ = ‖QuotientGroup.mk x‖

Goal state after:
case mk
M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x✝¹ : M ⧸ S
m : M
r ε : ℝ
x✝ : M ⧸ ⊥
x : M
⊢ ‖x‖ = ‖↑x‖
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:

Tactic:
_ ≤ ‖k‖ * ‖a‖ := (norm_mk_le ..).trans (norm_smul_le k a)
        _ ≤ _ := (sub_lt_iff_lt_add'.mp h.1).le

Goal state after: