mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
⊢ IsComplement (↑H) T ↔ ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! t, Quotient.mk'' ↑t = q

Tactic:
isComplement_iff_existsUnique_mul_inv_mem,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
⊢ (∀ (g : G), ∃! t, g * (↑t)⁻¹ ∈ ↑H) ↔ ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! t, Quotient.mk'' ↑t = q
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
⊢ g * (↑(hST.equiv g).2)⁻¹ = ↑⟨1, h1⟩

Tactic:
equiv_snd_eq_self_of_mem_of_one_mem _ h1 hg,

Goal state after:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
⊢ g * (↑⟨g, hg⟩)⁻¹ = ↑⟨1, h1⟩
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 γ
ω : Type u_4
mω : MeasurableSpace ω
υ : Measure ω
inst✝² : SFinite μ
inst✝¹ : SFinite τ
inst✝ : SFinite υ
f : α → β
g : γ → ω
hf : QuasiMeasurePreserving f μ ν
hg : QuasiMeasurePreserving g τ υ
⊢ (map f μ).prod (map g τ) ≪ ν.prod υ

Tactic:
exact hf.absolutelyContinuous.prod hg.absolutelyContinuous

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

Goal state before:
pp: 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
⊢ (map (fun x ↦ g * x) (comap (⇑f) μ)) s = (comap (⇑f) μ) s

Tactic:
map_apply (by fun_prop) hs

Goal state after:
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
⊢ (comap (⇑f) μ) ((fun x ↦ g * x) ⁻¹' s) = (comap (⇑f) μ) s
Module: Mathlib.MeasureTheory.Group.Measure

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

Tactic:
map_apply (by fun_prop) hs

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
H : Type u_3
inst✝² : Group H
mH : MeasurableSpace H
inst✝¹ : MeasurableMul H
μ : Measure H
inst✝ : μ.IsMulRightInvariant
f : G →* H
hf : MeasurableEmbedding ⇑f
g : G
s : Set G
hs : MeasurableSet s
⊢ (comap (⇑f) μ) ((fun x ↦ x * g) ⁻¹' s) = (comap (⇑f) μ) s
Module: Mathlib.MeasureTheory.Measure.Prod

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

Tactic:
simp only [h, snd_zero]

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : SFinite ν
ρ : Measure (α × β)
inst✝ : IsZeroOrProbabilityMeasure ρ
h : ρ = 0
⊢ IsZeroOrProbabilityMeasure 0
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x : G
⊢ (f ⋆ₘₗ[μ] g ⋆ₘₗ[μ] k) x = ((f ⋆ₘₗ[μ] g) ⋆ₘₗ[μ] k) x

Tactic:
simp only [mlconvolution_def]

Goal state after:
G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x : G
⊢ ∫⁻ (y : G), f y * ∫⁻ (y_1 : G), g y_1 * k (y_1⁻¹ * (y⁻¹ * x)) ∂μ ∂μ =
    ∫⁻ (y : G), (∫⁻ (y_1 : G), f y_1 * g (y_1⁻¹ * y) ∂μ) * k (y⁻¹ * x) ∂μ
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
⊢ (f ⋆ₘₗ[μ] g) x = (g ⋆ₘₗ[μ] f) x

Tactic:
simp only [mlconvolution_def]

Goal state after:
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
⊢ ∫⁻ (y : G), f y * g (y⁻¹ * x) ∂μ = ∫⁻ (y : G), g y * f (y⁻¹ * x) ∂μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : NullMeasurableSet s μ
t : Set α := toMeasurable μ s
A : ∫⁻ (a : α) in t, f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
B : (μ.withDensity f) t = (μ.withDensity f) s
⊢ (μ.withDensity f) s = ∫⁻ (a : α) in s, f a ∂μ

Tactic:
rw [← A, ← B]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : NullMeasurableSet s μ
t : Set α := toMeasurable μ s
A : ∫⁻ (a : α) in t, f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
B : (μ.withDensity f) t = (μ.withDensity f) s
⊢ (μ.withDensity f) t = ∫⁻ (a : α) in t, f 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✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
hν : ν ≠ 0
⊢ μ ≪ ν

Tactic:
refine AbsolutelyContinuous.mk fun s sm hνs => ?_

Goal state after:
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
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : ν s = 0
⊢ μ s = 0
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: case refine_2
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : TopologicalSpace G
inst✝² : BorelSpace G
μ : Measure G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h : μ.InnerRegularCompactLTTop
s : Set G
s_meas : MeasurableSet s
μs : μ s ≠ ∞
r : ℝ≥0∞
hr : r < μ s
K : Set G
Ks : K ⊆ s
K_comp : IsCompact K
hK : r < μ K
⊢ r < μ (closure[inst✝³] K)

Tactic:
· rwa [K_comp.measure_closure]

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
s✝ : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
hμs : μ' s ≠ ∞
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
a✝ : μ' A < ∞
h3A : ν' A⁻¹ < ∞
h1 : μ' s * ν' A⁻¹ = ∫⁻ (x : G), A.indicator (fun j ↦ ν' ((fun x ↦ x * j) ⁻¹' s) * (1 ∘ Inv.inv) j) x ∂μ'
⊢ ∫⁻ (x : G) in A, ν' ((fun y ↦ y * x) ⁻¹' s) ∂μ' ≠ ∞

Tactic:
Function.comp,

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s✝ : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
hμs : μ' s ≠ ∞
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
a✝ : μ' A < ∞
h3A : ν' A⁻¹ < ∞
h1 : μ' s * ν' A⁻¹ = ∫⁻ (x : G), A.indicator (fun j ↦ ν' ((fun x ↦ x * j) ⁻¹' s) * 1 j⁻¹) x ∂μ'
⊢ ∫⁻ (x : G) in A, ν' ((fun y ↦ y * x) ⁻¹' s) ∂μ' ≠ ∞
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s✝ : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
hμs : μ' s ≠ ∞
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
a✝ : μ' A < ∞
h3A : ν' A⁻¹ < ∞
h1 : μ' s * ∫⁻ (a : G) in A⁻¹, 1 a ∂ν' = ∫⁻ (x : G), ν' ((fun z ↦ z * x) ⁻¹' s) * A⁻¹.indicator 1 x⁻¹ ∂μ'
⊢ ∫⁻ (x : G) in A, ν' ((fun y ↦ y * x) ⁻¹' s) ∂μ' ≠ ∞

Tactic:
simp_rw [Pi.one_apply, setLIntegral_one, ← image_inv_eq_inv, indicator_image inv_injective,
    image_inv_eq_inv, ← indicator_mul_right _ fun x => ν' ((· * x) ⁻¹' s), Function.comp,
    Pi.one_apply, mul_one] at h1

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s✝ : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
hμs : μ' s ≠ ∞
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
a✝ : μ' A < ∞
h3A : ν' A⁻¹ < ∞
h1 : μ' s * ν' A⁻¹ = ∫⁻ (x : G), A.indicator (fun j ↦ ν' ((fun x ↦ x * j) ⁻¹' s)) x ∂μ'
⊢ ∫⁻ (x : G) in A, ν' ((fun y ↦ y * x) ⁻¹' s) ∂μ' ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : BorelSpace β
μ : Measure β
inst✝ : μ.Regular
f : α → β
hf : IsOpenEmbedding f
this✝ : (comap f μ).OuterRegular
this : IsFiniteMeasureOnCompacts (comap f μ)
⊢ (comap f μ).Regular

Tactic:
exact ⟨InnerRegularWRT.comap Regular.innerRegular hf.measurableEmbedding
    (fun _ hU ↦ hf.isOpen_iff_image_isOpen.mp hU)
    (fun _ hKrange hK ↦ hf.isInducing.isCompact_preimage' hK hKrange)⟩

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : R1Space α
inst✝¹ : BorelSpace α
inst✝ : μ.Regular
A : Set α
h'A : μ A ≠ ∞
this : (μ.restrict A).WeaklyRegular
V : Set α
⊢ IsOpen[inst✝³] V → ∀ r < (μ.restrict A) V, ∃ K ⊆ V, IsCompact K ∧ r < (μ.restrict A) K

Tactic:
hV

Goal state after:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : R1Space α
inst✝¹ : BorelSpace α
inst✝ : μ.Regular
A : Set α
h'A : μ A ≠ ∞
this : (μ.restrict A).WeaklyRegular
V : Set α
hV : IsOpen[inst✝³] V
⊢ ∀ r < (μ.restrict A) V, ∃ K ⊆ V, IsCompact K ∧ r < (μ.restrict A) K
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
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : a < 0
this : Tendsto (fun x ↦ (a * x + b) * x + c) atTop atBot
x : K
hx : (a * x + b) * x + c < 0
⊢ a * x * x + b * x + c < 0

Tactic:
← add_mul

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : a < 0
this : Tendsto (fun x ↦ (a * x + b) * x + c) atTop atBot
x : K
hx : (a * x + b) * x + c < 0
⊢ (a * x + b) * x + c < 0
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: ⊢ √0 = 0

Tactic:
by simp [Real.sqrt]

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

Goal state before:
pp: ⊢ √1 = 1

Tactic:
by simp [Real.sqrt]

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

Goal state before:
pp: x : ℝ
⊢ √x / x = 1 / √x

Tactic:
rw [← div_sqrt, one_div_div, div_sqrt]

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

Goal state before:
pp: z w : ℂ
⊢ ‖z + w‖ * ‖z + w‖ ≤ (‖z‖ + ‖w‖) * (‖z‖ + ‖w‖)

Tactic:
by
    rw [norm_mul_self_eq_normSq, add_mul_self_eq, norm_mul_self_eq_normSq, norm_mul_self_eq_normSq,
      add_right_comm, normSq_add, mul_assoc, norm_def, norm_def, ← Real.sqrt_mul <| normSq_nonneg z,
      ← normSq_conj w, ← map_mul]
    gcongr
    exact re_le_norm (z * conj w)

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

Goal state before:
pp: z : ℂ
⊢ dist ((starRingEnd ℂ) z) z = 2 * |z.im|

Tactic:
rw [dist_of_re_eq (conj_re z), conj_im, dist_comm, Real.dist_eq, sub_neg_eq_add, ← two_mul,
    _root_.abs_mul, abs_of_pos (zero_lt_two' ℝ)]

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

Goal state before:
pp: s s₁ t t₁ : Set ℝ
⊢ s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅

Tactic:
by
  convert! prod_subset_prod_iff
  exact reProdIm_subset_iff

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

Goal state before:
pp: a₁ a₂ b : ℝ
⊢ (fun x ↦ ↑x + ↑b * I) '' [[a₁, a₂]] = [[a₁, a₂]] ×ℂ {b}

Tactic:
rw [← preimage_equivRealProd_prod]

Goal state after:
a₁ a₂ b : ℝ
⊢ (fun x ↦ ↑x + ↑b * I) '' [[a₁, a₂]] = ⇑equivRealProd ⁻¹' [[a₁, a₂]] ×ˢ {b}
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: a b₁ b₂ : ℝ
⊢ (fun y ↦ ↑a + ↑y * I) '' [[b₁, b₂]] = {a} ×ℂ [[b₁, b₂]]

Tactic:
rw [← preimage_equivRealProd_prod]

Goal state after:
a b₁ b₂ : ℝ
⊢ (fun y ↦ ↑a + ↑y * I) '' [[b₁, b₂]] = ⇑equivRealProd ⁻¹' {a} ×ˢ [[b₁, b₂]]
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: case hb
ι : Type u_1
R : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : ExistsAddOfLE R
inst✝¹ : Module ℚ≥0 R
inst✝ : PosSMulMono ℚ≥0 R
s : Finset ι
f g : ι → R
⊢ (∑ x ∈ s, f x * g x) ^ 2 ≤ (∑ x ∈ s, f x ^ 2) * ∑ x ∈ s, g x ^ 2

Tactic:
exact sum_mul_sq_le_sq_mul_sq ..

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

Goal state before:
pp: E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : StarAddMonoid E
inst✝ : NormedStarGroup E
x : E
r : ℝ
⊢ (sphere x r)⋆ = sphere x⋆ r

Tactic:
by
  simpa using star_isometry.preimage_sphere (star x) r

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
x u : R
hu : u ∈ unitary R
⊢ Commute u x ↔ u * x * star u = x

Tactic:
simpa using! (Unitary.toUnits ⟨u, hu⟩).commute_iff_mul_inv_cancel

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

Goal state before:
pp: case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) = (algebraMap ℝ A) x₁ * (algebraMap ℝ A) x₂ + y₁ • I' * y₂ • I'

pp: case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (x₁ * y₂ + y₁ * x₂) • I' = (algebraMap ℝ A) x₁ * y₂ • I' + y₁ • I' * (algebraMap ℝ A) x₂

Tactic:
· rw [smul_mul_smul_comm, hf, smul_neg, ← algebraMap_eq_smul_one, ← sub_eq_add_neg,
      ← map_mul, ← map_sub]

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

Goal state before:
pp: A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : ℝ
b : ↥(skewAdjoint A)
⊢ ↑⟨-I • ↑(a • b), ⋯⟩ = ↑((RingHom.id ℝ) a • ⟨-I • ↑b, ⋯⟩)

Tactic:
simp [smul_comm I]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ re z * re z ≤ ‖z‖ * ‖z‖

Tactic:
mul_self_norm

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ re z * re z ≤ normSq z
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ im z * im z ≤ ‖z‖ * ‖z‖

Tactic:
mul_self_norm

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ im z * im z ≤ normSq z
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:
by
  rw [mul_conj, ← ofReal_pow]; simp [-map_pow]

Goal state after:
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.toEquiv

Tactic:
exact e.toHomeomorphSourceTarget.isInducing

Goal state after:
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
f : Y → Z
s : Set Y
x : Y
h : x ∈ e.target
⊢ Tendsto f (𝓝[s] x) (𝓝 (f x)) ↔ Tendsto (f ∘ ↑e) (𝓝[↑e ⁻¹' s] ↑e.symm x) (𝓝 ((f ∘ ↑e) (↑e.symm x)))

Tactic:
← @tendsto_map'_iff _ _ _ _ e,

Goal state after:
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
f : Y → Z
s : Set Y
x : Y
h : x ∈ e.target
⊢ Tendsto f (𝓝[s] x) (𝓝 (f x)) ↔ Tendsto f (map (↑e) (𝓝[↑e ⁻¹' s] ↑e.symm x)) (𝓝 ((f ∘ ↑e) (↑e.symm x)))
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝² : RCLike K
G : Type u_3
inst✝¹ : Finite G
inst✝ : AddCommGroup G
ψ : AddChar G K
x : G
⊢ ψ (-x) = (starRingEnd K) (ψ x)

Tactic:
rw [map_neg_eq_inv, inv_apply_eq_conj]

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
l : Filter α
⊢ IsBigOWith c l f g ↔ ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
rw [IsBigOWith_def]

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

Goal state before:
pp: α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
⊢ f =O[l] g ↔ ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖

Tactic:
by
  refine ⟨fun h => ?mp, fun h => ?mpr⟩
  case mp =>
    rw [isBigO_iff'] at h
    obtain ⟨c, ⟨hc_pos, hc⟩⟩ := h
    refine ⟨c⁻¹, ⟨by positivity, ?_⟩⟩
    filter_upwards [hc] with x hx
    rwa [inv_mul_le_iff₀ (by positivity)]
  case mpr =>
    rw [isBigO_iff']
    obtain ⟨c, ⟨hc_pos, hc⟩⟩ := h
    refine ⟨c⁻¹, ⟨by positivity, ?_⟩⟩
    filter_upwards [hc] with x hx
    rwa [← inv_inv c, inv_mul_le_iff₀ (by positivity)] at hx

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
f : α → E
g' : α → F'
l : Filter α
⊢ (f =O[l] fun x ↦ ‖g' x‖) ↔ f =O[l] g'

Tactic:
by
  simp only [IsBigO_def]
  exact exists_congr fun _ => isBigOWith_norm_right

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

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ
hf : 1 ≤ᶠ[l] f
m n : ℕ
h : n ≤ m
⊢ IsBigOWith 1 l (f ^ n) (f ^ m)

Tactic:
rw [IsBigOWith_def]

Goal state after:
α : Type u_1
l : Filter α
f : α → ℝ
hf : 1 ≤ᶠ[l] f
m n : ℕ
h : n ≤ m
⊢ ∀ᶠ (x : α) in l, ‖(f ^ n) x‖ ≤ 1 * ‖(f ^ m) x‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x a p : ℂ
n : ℕ
⊢ cexp (a * ↑n * x / p) = cexp (a * x / p) ^ n

Tactic:
rw [← Complex.exp_nsmul]

Goal state after:
x a p : ℂ
n : ℕ
⊢ cexp (a * ↑n * x / p) = cexp (n • (a * x / p))
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
R : Type u_13
inst✝ : SeminormedRing R
c : ℝ
l : Filter α
u v φ : α → R
hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c
h : u =ᶠ[l] φ * v
⊢ IsBigOWith c l u v

Tactic:
by
  simp only [IsBigOWith_def]
  refine h.symm.rw (fun x a => ‖a‖ ≤ c * ‖v x‖) (hφ.mono fun x hx => ?_)
  simp only [Pi.mul_apply]
  refine (norm_mul_le _ _).trans ?_
  gcongr

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

Goal state before:
pp: case calc_3
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ∑ i ∈ range k, ‖x‖ ^ n / ↑n.factorial * (‖x‖ ^ i / ↑n.succ ^ i) ≤ ‖x‖ ^ n / ↑n.factorial * 2

Tactic:
rw [← mul_sum]

Goal state after:
case calc_3
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ‖x‖ ^ n / ↑n.factorial * ∑ i ∈ range k, ‖x‖ ^ i / ↑n.succ ^ i ≤ ‖x‖ ^ n / ↑n.factorial * 2
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
by rw [← ofReal_tan_ofReal_re, ofReal_im]

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

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖sin x - (x - x ^ 3 / 6)‖ =
    ‖(cexp (-x * I) - ∑ m ∈ range 5, (-x * I) ^ m / ↑m.factorial) * I / 2 -
        (cexp (x * I) - ∑ m ∈ range 5, (x * I) ^ m / ↑m.factorial) * I / 2‖

Tactic:
simp [sin, field, Finset.sum_range_succ, Nat.factorial]
      grind [I_sq, two_ne_zero]

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

Goal state before:
pp: x : ℝ
⊢ sin x * sin x ≤ 1

Tactic:
by simp only [← sq, sin_sq_le_one]

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

Goal state before:
pp: case hab
x : ℝ
hx : |x| ≤ 1
⊢ |x| * |x| ≤ 1

Tactic:
exact mul_le_one₀ hx (abs_nonneg _) hx

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

Goal state before:
pp: E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h✝ : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec✝ :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
⊢ ∃ c, ∀ᶠ (x : ℕ) in atTop, ‖f x‖ ≤ c * ‖g x‖

Tactic:
obtain ⟨n₁, H₁, H₂⟩ := (eventually_ge_atTop n₀).and hrec |>.exists

Goal state after:
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h✝ : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec✝ :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
⊢ ∃ c, ∀ᶠ (x : ℕ) in atTop, ‖f x‖ ≤ c * ‖g x‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖cexp (-(↑x / 2 * I)) * (cexp ((↑x / 2 + -(↑x / 2)) * I) - cexp (↑x / 2 * I + ↑x / 2 * I)) * I‖

Tactic:
← add_mul

Goal state after:
x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖cexp (-(↑x / 2 * I)) * (cexp ((↑x / 2 + -(↑x / 2)) * I) - cexp ((↑x / 2 + ↑x / 2) * I)) * I‖
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: ⊢ comap rexp (𝓝[>] 0) = atBot

Tactic:
← map_exp_atBot,

Goal state after:
⊢ comap rexp (Filter.map rexp atBot) = atBot
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: α : Type u_1
l : Filter α
f : ℝ → α
⊢ Tendsto (fun x ↦ f (rexp x)) atBot l ↔ Tendsto f (𝓝[>] 0) l

Tactic:
← map_exp_atBot,

Goal state after:
α : Type u_1
l : Filter α
f : ℝ → α
⊢ Tendsto (fun x ↦ f (rexp x)) atBot l ↔ Tendsto f (Filter.map rexp atBot) l
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: ⊢ comap re (comap Real.exp atTop) = comap re atTop

Tactic:
Real.comap_exp_atTop

Goal state after:
⊢ comap re atTop = comap re atTop
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ {x} * ball y δ = ball (x * y) δ

Tactic:
simp only [preimage_mul_ball, image_mul_left, singleton_mul, div_inv_eq_mul, mul_comm y x]

Goal state after: