mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ
⊢ μ (L n) = ↑(n + 1) * μ K

Tactic:
induction n with
    | zero => simp only [L, one_mul, Nat.cast_one, iterate_zero, id, Nat.zero_add]
    | succ n IH =>
      calc
        μ (L (n + 1)) = μ (L n) + μ (g (L n) • K) := by
          simp_rw [L, iterate_succ']
          exact measure_union' (hg _ (Lcompact _)) (Lclosed _).measurableSet
        _ = (n + 1 + 1 : ℕ) * μ K := by
          simp only [IH, measure_smul, add_mul, Nat.cast_add, Nat.cast_one, one_mul]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ (μ.restrict s).withDensity 1 = μ.restrict s

Tactic:
withDensity_one

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ μ.restrict s = μ.restrict 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⁻¹ = ∫⁻ (x : G), ν' ((fun z ↦ z * x) ⁻¹' s) * A.indicator (1 ∘ Inv.inv) x ∂μ'
⊢ ∫⁻ (x : G) in A, ν' ((fun y ↦ y * x) ⁻¹' s) ∂μ' ≠ ∞

Tactic:
← indicator_mul_right _ fun x => ν' ((· * x) ⁻¹' s),

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 ∘ Inv.inv) 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
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
⊢ μ' = (μ' s / ν' s) • ν'

Tactic:
ext1 t -
  rw [Measure.smul_apply, smul_eq_mul, mul_comm, ← mul_div_assoc, mul_comm,
    measure_mul_measure_eq μ' ν' s t h2s h3s, mul_div_assoc, ENNReal.mul_div_cancel h2s h3s]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
this : (f * fun x ↦ (f x)⁻¹) ≤ᵐ[μ] 1
⊢ μ.withDensity 1 ≤ μ

Tactic:
withDensity_one

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
this : (f * fun x ↦ (f x)⁻¹) ≤ᵐ[μ] 1
⊢ μ ≤ μ
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 ≠ ∞
this : (f * fun x ↦ (f x)⁻¹) =ᵐ[μ] 1
⊢ μ.withDensity 1 = μ

Tactic:
withDensity_one

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
this : (f * fun x ↦ (f x)⁻¹) =ᵐ[μ] 1
⊢ μ = μ
Module: Mathlib.Analysis.Complex.Order

Goal state before:
pp: z : ℂ
h : z.re = 0
⊢ z.re ^ 2 - z.im ^ 2 ≤ 0 ∧ (z.re = 0 ∨ z.im = 0)

Tactic:
by simpa [h] using sq_nonneg z.im

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0
hf : Continuous f
⊢ IsLocallyFiniteMeasure (μ.withDensity fun x ↦ ↑(f x))

Tactic:
by
  refine ⟨fun x ↦ ?_⟩
  rcases (μ.finiteAt_nhds x).exists_mem_basis ((nhds_basis_opens' x).restrict_subset
    ((hf.tendsto x).eventually_le_const (lt_add_one _))) with ⟨U, ⟨⟨hUx, hUo⟩, hUf⟩, hμU⟩
  refine ⟨U, hUx, ?_⟩
  rw [withDensity_apply _ hUo.measurableSet]
  exact setLIntegral_lt_top_of_bddAbove hμU.ne ⟨f x + 1, forall_mem_image.2 hUf⟩

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

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f g : NormedAddGroupHom V₁ V₂
h : f.toAddMonoidHom = g.toAddMonoidHom
⊢ ⇑f = ⇑g

Tactic:
by rw [← coe_toAddMonoidHom f, ← coe_toAddMonoidHom g, h]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Ring 𝕜
inst✝⁶ : Ring 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), ‖f x‖ = a * ‖x‖
y : F
⊢ ‖f.symm y‖ = a⁻¹ * ‖y‖

Tactic:
simpa [eq_inv_mul_iff_mul_eq₀ (ne_of_gt ha)] using (hf (f.symm y)).symm

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (x y : ℝ), (algebraMap ℝ 𝕜) (x * y) = (algebraMap ℝ 𝕜) x * (algebraMap ℝ 𝕜) y

Tactic:
by subst h''; exact h.algebraMap.map_mul'

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

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

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

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

Goal state after:
case mpr
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
⊢ f =O[l] g
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'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
⊢ f =O[l] g

Tactic:
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.Tactic.NormNum.NatFactorial

Goal state before:
pp: n x l y : ℕ
h₁ : IsNat n x
h₂ : IsNat l y
a : ℕ
p : x.ascFactorial y = a
⊢ IsNat (n.ascFactorial l) a

Tactic:
by
  constructor
  simp [h₁.out, h₂.out, ← p]

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
f : α → E
g'' : α → F''
l : Filter α
h : ∀ᶠ (x : α) in l, g'' x ≠ 0
⊢ f =O[l] g'' ↔ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f x‖ / ‖g'' x‖

Tactic:
by
  simp only [isBigO_iff, IsBoundedUnder, IsBounded, eventually_map]
  exact
    exists_congr fun c =>
      eventually_congr <| h.mono fun x hx => (div_le_iff₀ <| norm_pos_iff.2 hx).symm

Goal state after:
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'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
⊢ sSup (C '' ↑s) * ∑ i ∈ s, ‖B i x‖ = sSup (C '' ↑s) * ‖∑ i ∈ s, ‖B i x‖‖

Tactic:
by
      congr; rw [Real.norm_of_nonneg (Finset.sum_nonneg (fun _ _ ↦ norm_nonneg _))]

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

Goal state before:
pp: α : Type u_1
F : Type u_4
E'' : Type u_9
inst✝¹ : Norm F
inst✝ : NormedAddCommGroup E''
g : α → F
l : Filter α
c : E''
hc : c ≠ 0
⊢ (fun _x ↦ c) =o[l] g ↔ Tendsto (fun x ↦ ‖g x‖) l atTop

Tactic:
by
  simp only [← isLittleO_one_left_iff ℝ]
  exact ⟨(isBigO_const_const (1 : ℝ) hc l).trans_isLittleO,
    (isBigO_const_one ℝ c l).trans_isLittleO⟩

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)
⊢ ⟨fun n ↦ ∑ m ∈ range n, x ^ m / ↑m.factorial, ⋯⟩ * ⟨fun n ↦ ∑ m ∈ range n, y ^ m / ↑m.factorial, ⋯⟩ ≈
    ⟨fun n ↦ ∑ m ∈ range n, (x + y) ^ m / ↑m.factorial, ⋯⟩

Tactic:
simp only [hj]

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)
⊢ ⟨fun n ↦ ∑ m ∈ range n, x ^ m / ↑m.factorial, ⋯⟩ * ⟨fun n ↦ ∑ m ∈ range n, y ^ m / ↑m.factorial, ⋯⟩ ≈
    ⟨fun n ↦ ∑ i ∈ range n, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial), ⋯⟩
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cosh x ^ 2 - sinh x ^ 2 = 1

Tactic:
rw [sq_sub_sq, cosh_add_sinh, cosh_sub_sinh, ← exp_add, add_neg_cancel, exp_zero]

Goal state after:
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:
by
    rwa [isLittleO_one_iff] at h

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

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ range j with n ≤ m, ‖x ^ n * (x ^ (m - n) / ↑m.factorial)‖ ≤
    ∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * (1 / ↑m.factorial)

Tactic:
by
      simp_rw [Complex.norm_mul, Complex.norm_pow, Complex.norm_div, norm_natCast]
      gcongr
      rw [Complex.norm_pow]
      exact pow_le_one₀ (norm_nonneg _) hx

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

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

Tactic:
hj,

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

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖∑ m ∈ range j, x ^ m / ↑m.factorial - ∑ m ∈ range n, x ^ m / ↑m.factorial‖ ≤ ↑(const abs (‖x‖ ^ n * Real.exp ‖x‖)) j

Tactic:
rw [← sum_Ico_eq_sub _ hj]

Goal state after:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖∑ k ∈ Ico n j, x ^ k / ↑k.factorial‖ ≤ ↑(const abs (‖x‖ ^ n * Real.exp ‖x‖)) j
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
k : ℕ
hk : a ≤ k • ε
n : ℕ
hnm : n ≥ m
⊢ a + a < k • ε + (k • ε + ε)

Tactic:
exact add_lt_add_of_le_of_lt hk (lt_of_le_of_lt hk (lt_add_of_pos_right _ ε0))

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

Goal state before:
pp: α : Type u_1
inst✝² : NormedRing α
inst✝¹ : NormSMulClass ℤ α
inst✝ : Nontrivial α
⊢ Tendsto (fun x ↦ ‖↑x‖) atTop atTop

Tactic:
simpa [norm_natCast_eq_mul_norm_one] using tendsto_natCast_atTop_atTop
    |>.atTop_mul_const (norm_pos_iff.mpr one_ne_zero)

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
x y : R ⧸ I
ε : ℝ
hε : 0 < ε
this :
  ∃ ia,
    (0 < ia.1 ∧ 0 < ia.2) ∧ ∀ x_1 ∈ ball ‖x‖ ia.1 ×ˢ ball ‖y‖ ia.2, x_1.1 * x_1.2 ∈ ball ((‖x‖, ‖y‖).1 * (‖x‖, ‖y‖).2) ε
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖ + ε

Tactic:
simp only [Set.mem_prod, mem_ball, and_imp, Prod.forall, Prod.exists] at this

Goal state after:
M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
x y : R ⧸ I
ε : ℝ
hε : 0 < ε
this : ∃ a b, (0 < a ∧ 0 < b) ∧ ∀ (a_1 b_1 : ℝ), dist a_1 ‖x‖ < a → dist b_1 ‖y‖ < b → dist (a_1 * b_1) (‖x‖ * ‖y‖) < ε
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖ + ε
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_2
inst✝¹ : SeminormedRing R
inst✝ : NormMulClass R
x : R
⊢ Tendsto (fun n ↦ x ^ n) atTop (𝓝 0) ↔ ‖x‖ < 1

Tactic:
refine ⟨?_, tendsto_pow_atTop_nhds_zero_of_norm_lt_one⟩

Goal state after:
R : Type u_2
inst✝¹ : SeminormedRing R
inst✝ : NormMulClass R
x : R
⊢ Tendsto (fun n ↦ x ^ n) atTop (𝓝 0) → ‖x‖ < 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ 2 * s * c = sin (2 * θ)

Tactic:
by rw [sin_two_mul]

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

Goal state before:
pp: θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ sin (2 * θ) * c + cos (2 * θ) * s = 2 * s * c * c + cos (2 * θ) * s

Tactic:
by rw [sin_two_mul]

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

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

Tactic:
sin_pi_div_three,

Goal state after:
⊢ √3 / 2 / cos (π / 3) = √3
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: K : Type u_4
inst✝ : NormedDivisionRing K
ξ : K
⊢ (Summable fun n ↦ ξ ^ n) ↔ ‖ξ‖ < 1

Tactic:
by
  refine ⟨fun h ↦ ?_, summable_geometric_of_norm_lt_one⟩
  obtain ⟨k : ℕ, hk : dist (ξ ^ k) 0 < 1⟩ :=
    (h.tendsto_cofinite_zero.eventually (ball_mem_nhds _ zero_lt_one)).exists
  simp only [norm_pow, dist_zero_right] at hk
  rw [← one_pow k] at hk
  exact lt_of_pow_lt_pow_left₀ _ zero_le_one hk

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

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n ↦ ↑((n + k).choose k) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
n : ℕ
⊢ n ∈ Set.Ioi k → ‖↑((n + k).choose k)‖ ≤ 2 ^ k * ‖↑(n ^ k)‖

Tactic:
(hn : k < n)

Goal state after:
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n ↦ ↑((n + k).choose k) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
n : ℕ
hn : k < n
⊢ ‖↑((n + k).choose k)‖ ≤ 2 ^ k * ‖↑(n ^ k)‖
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case e'_6
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n ↦ ↑((n + k).choose k) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
I1 : Summable fun n ↦ ‖↑((n + k).choose k) * r ^ n‖
⊢ (1 - r)⁻¹ʳ ^ (k + 1 + 1) = (1 - r)⁻¹ʳ ^ (k + 1) * (1 - r)⁻¹ʳ

Tactic:
pow_succ

Goal state after:
case e'_6
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n ↦ ↑((n + k).choose k) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
I1 : Summable fun n ↦ ‖↑((n + k).choose k) * r ^ n‖
⊢ (1 - r)⁻¹ʳ ^ (k + 1) * (1 - r)⁻¹ʳ = (1 - r)⁻¹ʳ ^ (k + 1) * (1 - r)⁻¹ʳ
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case refine_1.inr
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : s ∈ 𝓝 (const X c)
S : Set (Set X × Set Y)
hSf : S.Finite
hSsub : {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst✝] U
hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c)) K U
this : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c
i : ι
hpi : p i
hi : U i ⊆ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2
f : C(X, Y)
hf : f ∈ {f | MapsTo ⇑f (⋃ KU ∈ S, KU.1, i).1 (U (⋃ KU ∈ S, KU.1, i).2)}
K : Set X
V : Set Y
hKV : (K, V) ∈ S
hKne : K.Nonempty
⊢ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ⊆ V

Tactic:
exact (biInter_subset_of_mem hKV).trans <| iInter_subset _ hKne

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactPair Y Z
f : C(X, Y)
g : C(Y, Z)
K : Set X
hK : IsCompact K
⊢ ∀ (U : Set Z),
    IsOpen[inst✝¹] U →
      MapsTo (⇑((f, g).2.comp (f, g).1)) K U → ∀ᶠ (a : C(X, Y) × C(Y, Z)) in 𝓝 (f, g), MapsTo (⇑(a.2.comp a.1)) K U

Tactic:
U

Goal state after:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactPair Y Z
f : C(X, Y)
g : C(Y, Z)
K : Set X
hK : IsCompact K
U : Set Z
⊢ IsOpen[inst✝¹] U →
    MapsTo (⇑((f, g).2.comp (f, g).1)) K U → ∀ᶠ (a : C(X, Y) × C(Y, Z)) in 𝓝 (f, g), MapsTo (⇑(a.2.comp a.1)) K U
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace T
K✝ : Set X
U : Set Y
inst✝ : RegularSpace Y
f : C(X, Y)
K : Set X
hK : IsCompact K
⊢ ∀ (U : Set Y), IsOpen[inst✝³] U → MapsTo (⇑f) K U → ∀ᶠ (a : C(X, Y)) in (𝓝 f).lift' closure, MapsTo (⇑(id a)) K U

Tactic:
U

Goal state after:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace T
K✝ : Set X
U✝ : Set Y
inst✝ : RegularSpace Y
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
⊢ IsOpen[inst✝³] U → MapsTo (⇑f) K U → ∀ᶠ (a : C(X, Y)) in (𝓝 f).lift' closure, MapsTo (⇑(id a)) K U
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case mp
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
⊢ (∃ f, Tendsto F l (𝓝 f)) → ∀ (s : Set X), IsCompact s → ∃ f, Tendsto (fun i ↦ restrict s (F i)) l (𝓝 f)

Tactic:
rintro ⟨f, hf⟩ s _

Goal state after:
case mp
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : C(X, Y)
hf : Tendsto F l (𝓝 f)
s : Set X
a✝ : IsCompact s
⊢ ∃ f, Tendsto (fun i ↦ restrict s (F i)) l (𝓝 f)
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ✝ : Path x y
a b : X
γ : Path a b
⊢ γ.extend (min 0 0) = a

Tactic:
by rw [min_self, γ.extend_zero]

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

Goal state before:
pp: ⊢ -sin (π / 2) = -1

Tactic:
sin_pi_div_two

Goal state after:
⊢ -1 = -1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ x < sin (π / 2) ↔ x < 1

Tactic:
sin_pi_div_two

Goal state after:
x : ℝ
⊢ x < 1 ↔ x < 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ -sin (π / 2) < x ↔ -1 < x

Tactic:
sin_pi_div_two

Goal state after:
x : ℝ
⊢ -1 < x ↔ -1 < x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr
x : ℂ
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ ↑‖x‖ * cexp (↑x.arg * I) = x

Tactic:
apply Complex.ext <;> simp [sin_arg, cos_arg hx, this, mul_comm ‖x‖]

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

Goal state before:
pp: x : ℝ
⊢ 0 ≤ arccos x

Tactic:
by
  unfold arccos; linarith [arcsin_le_pi_div_two x]

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

Goal state before:
pp: case succ.inr
x : ℝ
n : ℕ
ih : log (x ^ n) = ↑n * log x
hx : x ≠ 0
⊢ log (x ^ (n + 1)) = ↑(n + 1) * log x

Tactic:
· rw [pow_succ, log_mul (pow_ne_zero _ hx) hx, ih, Nat.cast_succ, add_mul, one_mul]

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

Goal state before:
pp: x : ℂ
⊢ ‖x‖ = 1 ↔ ∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x

Tactic:
rw [norm_eq_one_iff]

Goal state after:
x : ℂ
⊢ (∃ θ, cexp (↑θ * I) = x) ↔ ∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0 else cexp ((if x.arg = π then -(starRingEnd ℂ) (log x) else -log x) * n)) =
    if x.arg = π then
      (starRingEnd ℂ) (if x = 0 then if (starRingEnd ℂ) n = 0 then 1 else 0 else cexp (log x * (starRingEnd ℂ) n))⁻¹
    else (if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n))⁻¹

Tactic:
map_eq_zero,

Goal state after:
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0 else cexp ((if x.arg = π then -(starRingEnd ℂ) (log x) else -log x) * n)) =
    if x.arg = π then (starRingEnd ℂ) (if x = 0 then if n = 0 then 1 else 0 else cexp (log x * (starRingEnd ℂ) n))⁻¹
    else (if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
ψ : ℝ
⊢ θ.sin = Real.sin ψ ↔ θ = ↑ψ ∨ θ + ↑ψ = ↑π

Tactic:
by
  induction θ using Real.Angle.induction_on
  exact sin_eq_iff_coe_eq_or_add_eq_pi

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

Goal state before:
pp: ⊢ sin 0 = 0

Tactic:
rw [← coe_zero, sin_coe, Real.sin_zero]

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

Goal state before:
pp: x n : ℂ
⊢ (if (starRingEnd ℂ) x = 0 then if n = 0 then 1 else 0 else cexp (log ((starRingEnd ℂ) x) * n)) =
    if x.arg = π then if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n)
    else (starRingEnd ℂ) (if x = 0 then if (starRingEnd ℂ) n = 0 then 1 else 0 else cexp (log x * (starRingEnd ℂ) n))

Tactic:
map_eq_zero,

Goal state after:
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0 else cexp (log ((starRingEnd ℂ) x) * n)) =
    if x.arg = π then if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n)
    else (starRingEnd ℂ) (if x = 0 then if n = 0 then 1 else 0 else cexp (log x * (starRingEnd ℂ) n))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inl
θ : Angle
h : θ.sign = -1
⊢ -↑|θ.toReal| = θ

Tactic:
abs_of_neg (toReal_neg_iff_sign_neg.2 h),

Goal state after:
case inl
θ : Angle
h : θ.sign = -1
⊢ -↑(-θ.toReal) = θ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: p : ℝ × ℝ
hp_fst : 0 < p.1
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, 0 < x.1
x : ℝ × ℝ
hx : 0 < x.1
⊢ (fun x ↦ x.1 ^ x.2) x = (fun x ↦ rexp (log x.1 * x.2)) x

Tactic:
by
      dsimp only
      rw [rpow_def_of_pos hx]

Goal state after: