mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (a : α), (f * fun x ↦ ∫⁻ (y : β), φ (x, y) ∂ν) a ∂μ = ∫⁻ (a : α × β), φ a ∂(μ.prod ν).withDensity fun z ↦ f z.1

pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun x ↦ ∫⁻ (y : β), φ (x, y) ∂ν) μ

Tactic:
lintegral_withDensity_eq_lintegral_mul₀ _ hφ.aemeasurable,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (a : α), (f * fun x ↦ ∫⁻ (y : β), φ (x, y) ∂ν) a ∂μ = ∫⁻ (a : α × β), ((fun z ↦ f z.1) * φ) a ∂μ.prod ν

α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun z ↦ f z.1) (μ.prod ν)

α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun x ↦ ∫⁻ (y : β), φ (x, y) ∂ν) μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (x : α), ∫⁻ (y : β), φ (x, y) ∂ν.withDensity g ∂μ = ∫⁻ (a : α × β), φ a ∂(μ.prod ν).withDensity fun z ↦ g z.2

Tactic:
lintegral_withDensity_eq_lintegral_mul₀ _ hφ.aemeasurable,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (x : α), ∫⁻ (y : β), φ (x, y) ∂ν.withDensity g ∂μ = ∫⁻ (a : α × β), ((fun z ↦ g z.2) * φ) a ∂μ.prod ν

α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun z ↦ g z.2) (μ.prod ν)
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
⊢ (g.comp f).range = AddSubgroup.map g.toAddMonoidHom f.range

Tactic:
unfold range

Goal state after:
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
⊢ (g.comp f).toAddMonoidHom.range = AddSubgroup.map g.toAddMonoidHom f.toAddMonoidHom.range
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r s : R
x : ℂ
⊢ ((r + s) • x).re = (r • x + s • x).re

Tactic:
simp [smul_re, smul_im, add_smul]

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

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r s : R
x : ℂ
⊢ ((r + s) • x).im = (r • x + s • x).im

Tactic:
simp [smul_re, smul_im, add_smul]

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

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

Tactic:
by rw [re_add_im, conj_eq_re_sub_im]

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

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

Tactic:
by
  rw [abs_div, abs_norm]
  exact div_le_one_of_le₀ (abs_re_le_norm _) (norm_nonneg _)

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
hk : NormedField 𝕜
h : IsRCLikeNormedField 𝕜
⊢ RCLike 𝕜

Tactic:
choose p hp using h.out
  exact p.copy_of_normedField hk hp

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

Goal state before:
pp: case mp.succ
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : f =o[l] g
n : ℕ
this : 0 < ↑n.succ
⊢ ∀ᶠ (x : α) in l, ↑(n + 1) * ‖f x‖ ≤ ‖g x‖

Tactic:
exact (isBigOWith_inv this).1 (H.def' <| inv_pos.2 this)

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₁ : IsBigOWith c₁ l f₁ g₁
h₂ : IsBigOWith c₂ l f₂ g₂
⊢ IsBigOWith (max c₁ c₂) l (fun x ↦ f₁ x + f₂ x) fun x ↦ ‖g₁ x‖ + ‖g₂ x‖

Tactic:
by
  rw [IsBigOWith_def] at *
  filter_upwards [h₁, h₂] with x hx₁ hx₂
  calc
    ‖f₁ x + f₂ x‖ ≤ c₁ * ‖g₁ x‖ + c₂ * ‖g₂ x‖ := norm_add_le_of_le hx₁ hx₂
    _ ≤ (max c₁ c₂) * ‖g₁ x‖ + (max c₁ c₂) * ‖g₂ x‖ := by
        gcongr <;> simp [le_max_left _ _, le_max_right _ _]
    _ = (max c₁ c₂) * ‖‖g₁ x‖ + ‖g₂ x‖‖ := by
        rw [Real.norm_of_nonneg (add_nonneg (norm_nonneg _) (norm_nonneg _)), mul_add]

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

Goal state before:
pp: case succ
ε : ℝ
ε0 : ε > 0
j : ℕ
hj : j + 1 ≥ 1
⊢ ‖↑(exp' 0 - const (fun x ↦ ‖x‖) 1) (j + 1)‖ = 0

Tactic:
dsimp [exp']
    induction j with
    | zero => simp
    | succ j ih =>
      rw [← ih (by simp)]
      simp only [sum_range_succ, pow_succ]
      simp

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

Goal state before:
pp: x : ℂ
⊢ -(cosh x - sinh x) = -cexp (-x)

Tactic:
cosh_sub_sinh

Goal state after:
x : ℂ
⊢ -cexp (-x) = -cexp (-x)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
n : ℕ
h : 1 < n
⊢ (fun x ↦ ‖x‖ ^ n) =o[𝓝 0] fun x ↦ x

Tactic:
by
  have := @isLittleO_norm_pow_norm_pow E' _ _ _ h
  simp only [pow_one] at this
  exact isLittleO_norm_right.mp this

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

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

Tactic:
← div_pow

Goal state after:
case hbc
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ∑ x_1 ∈ range k, (‖x‖ / ↑n.succ) ^ x_1 ≤ 2
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''
hfg : f =O[atTop] g
l : Filter ℕ
h : ∀ᶠ (n : ℕ) in l, g n = 0 → f n = 0
⊢ f =O[l] g

Tactic:
obtain ⟨C, hC_pos, hC⟩ := bound_of_isBigO_nat_atTop hfg
  refine isBigO_iff.mpr ⟨C, ?_⟩
  filter_upwards [h] with x h
  by_cases hf : f x = 0
  · simp [hf, hC_pos]
  exact hC fun a ↦ hf (h a)

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

Goal state before:
pp: x : ℝ
⊢ ↑(sin (2 * x)) = ↑(2 * sin x * cos x)

Tactic:
simp [sin_two_mul]

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

Goal state before:
pp: x : ℝ
⊢ -(cosh x - sinh x) = -rexp (-x)

Tactic:
cosh_sub_sinh

Goal state after:
x : ℝ
⊢ -rexp (-x) = -rexp (-x)
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
two_sin

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

Goal state before:
pp: x : ℝ
⊢ sin x ≠ 0 ↔ ∀ (n : ℤ), ↑n * π ≠ x

Tactic:
by
  contrapose!; exact sin_eq_zero_iff

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

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
⊢ Ioo a b • sphere 0 r = ball 0 (b * r) \ closedBall 0 (a * r)

Tactic:
have : EqOn (‖·‖) id (Ioo a b) := fun x hx ↦ abs_of_pos (ha.trans_lt hx.1)

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
this : EqOn (fun x ↦ ‖x‖) id (Ioo a b)
⊢ Ioo a b • sphere 0 r = ball 0 (b * r) \ closedBall 0 (a * r)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f (b + 1)‖ ≤ r * ‖f b‖
n : ℕ
| ‖f N‖ * r ^ n

Tactic:
rw [mul_comm, ← zero_add N]

Goal state after:
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f (b + 1)‖ ≤ r * ‖f b‖
n : ℕ
| r ^ n * ‖f (0 + N)‖
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: G : Type u_4
inst✝² : InvolutiveInv G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousInv G
s : Set G
hs : IsPathConnected s
a : G
ha_mem : a ∈ s
ha : ∀ ⦃y : G⦄, y ∈ s → JoinedIn s a y
x : G
hx : x ∈ s⁻¹
⊢ JoinedIn s⁻¹ a⁻¹ x

Tactic:
by simpa using ha (mem_inv.mp hx) |>.map continuous_inv

Goal state after:
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
hU : IsOpen[inst✝³] U
hf : MapsTo (⇑f) K U
V : Set Y
hVo : IsOpen[inst✝³] V
hKV : ⇑f '' K ⊆ V
hVU : closure[inst✝³] V ⊆ U
⊢ ∀ᶠ (a : C(X, Y)) in (𝓝 f).lift' closure, MapsTo (⇑(id a)) K U

Tactic:
filter_upwards [mem_lift' (eventually_mapsTo hK hVo (mapsTo_iff_image_subset.2 hKV))] with g hg

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
hU : IsOpen[inst✝³] U
hf : MapsTo (⇑f) K U
V : Set Y
hVo : IsOpen[inst✝³] V
hKV : ⇑f '' K ⊆ V
hVU : closure[inst✝³] V ⊆ U
g : C(X, Y)
hg : g ∈ closure {x | MapsTo (⇑x) K V}
⊢ MapsTo (⇑(id g)) K U
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
T : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace T
s : Set T
f : T → X → Y
g : C(X, Y)
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ univ)
this : ∀ x ∈ s, Continuous[inst✝², inst✝¹] (f x)
x : ↑s
y : X
| mkD (f ↑x) g

Tactic:
mkD_of_continuous (this x x.2)

Goal state after:
X : Type u_2
Y : Type u_3
T : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace T
s : Set T
f : T → X → Y
g : C(X, Y)
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ univ)
this : ∀ x ∈ s, Continuous[inst✝², inst✝¹] (f x)
x : ↑s
y : X
| { toFun := f ↑x, continuous_toFun := ⋯ }
Module: Mathlib.Topology.Instances.AddCircle.Real

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
⊢ toAddCircle j = ↑(↑j.val / ↑N)

Tactic:
← toAddCircle_natCast,

Goal state after:
N : ℕ
inst✝ : NeZero N
j : ZMod N
⊢ toAddCircle j = toAddCircle ↑j.val
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case e_s
p x t : ℝ
ht : t ≠ 0
m : ℝ
⊢ m ∈ {m | ↑m = ↑(t * x)} ↔ m ∈ t • {m | ↑m = ↑x}

Tactic:
simp_rw [zmultiples, eq_iff_sub_mem, zsmul_eq_mul, mul_left_comm, ← smul_eq_mul, Set.range_smul]

Goal state after:
case e_s
p x t : ℝ
ht : t ≠ 0
m : ℝ
⊢ m ∈ {m | m - t • x ∈ { carrier := t • range fun i ↦ ↑i • p, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }} ↔
    m ∈ t • {m | m - x ∈ { carrier := range fun x ↦ ↑x • p, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }}
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
⊢ False

Tactic:
obtain ⟨hy₃, hy₄⟩ := hs hy₀

Goal state after:
case inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: ⊢ arg 0 = 0

Tactic:
simp [arg]

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

Goal state before:
pp: ⊢ (-1).arg = π

Tactic:
simp [arg]

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

Goal state before:
pp: ⊢ I.arg = π / 2

Tactic:
simp [arg]

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

Goal state before:
pp: ⊢ (-I).arg = -(π / 2)

Tactic:
simp [arg]

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ (↑(Real.log x)).im = (log ↑x).im

Tactic:
by rw [ofReal_im, log_im, arg_ofReal_of_nonneg hx]

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

Goal state before:
pp: case neg
x : ℂ
hx : ¬x.arg = π
⊢ ↑(Real.log ‖x‖) + ↑(-x.arg) * I = ↑(Real.log ‖x‖) + ↑x.arg * (starRingEnd ℂ) I

Tactic:
simp_rw [ofReal_neg, conj_I, mul_neg, neg_mul]

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ 2 * x / (x + 2) ≤ log (1 + x)

Tactic:
rw [le_log_iff_exp_le (by grind)]
  convert exp_le_two_add_div_two_sub (x := 2 * x / (x + 2)) (by positivity) _ using 1
  all_goals field_simp; grind

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

Goal state before:
pp: case neg
x : ℂ
hx : ¬x = 0
⊢ log ((starRingEnd ℂ) x) - ↑(Real.log (normSq x)) = if x.arg = π then -(starRingEnd ℂ) (log x) else -log x

pp: case neg.hr
x : ℂ
hx : ¬x = 0
⊢ 0 < (normSq x)⁻¹

pp: case neg.hx
x : ℂ
hx : ¬x = 0
⊢ (starRingEnd ℂ) x ≠ 0

Tactic:
log_conj_eq_ite

Goal state after:
case neg
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then log x else (starRingEnd ℂ) (log x)) - ↑(Real.log (normSq x)) =
    if x.arg = π then -(starRingEnd ℂ) (log x) else -log x

case neg.hr
x : ℂ
hx : ¬x = 0
⊢ 0 < (normSq x)⁻¹

case neg.hx
x : ℂ
hx : ¬x = 0
⊢ (starRingEnd ℂ) x ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case pos
α : Type u_1
f : α → ℝ
h : ∀ (a : α), 0 < f a
H : (support fun i ↦ log (f i)) = mulSupport f
H' : HasFiniteMulSupport f ↔ HasFiniteSupport fun a ↦ log (f a)
h' : HasFiniteMulSupport f
⊢ log (if h : HasFiniteMulSupport f then ∏ i ∈ Finite.toFinset h, f i else 1) =
    if h : HasFiniteSupport fun i ↦ log (f i) then ∑ i ∈ Finite.toFinset h, log (f i) else 0

Tactic:
simp [h', log_prod (fun a _ ↦ (h a).ne'), H'.mp h', H]

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

Goal state before:
pp: θ : Angle
⊢ 2 • θ = 0 ↔ θ = 0 ∨ θ = ↑π

Tactic:
by
  simp_rw [two_zsmul, ← two_nsmul, two_nsmul_eq_zero_iff]

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

Goal state before:
pp: y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 1 + y / x = rexp (log (x + y)) / rexp (log x)

Tactic:
exp_log,

Goal state after:
y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 1 + y / x = (x + y) / rexp (log x)

y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 0 < x + y
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 1 + y / x = (x + y) / rexp (log x)

pp: y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 0 < x + y

Tactic:
exp_log,

Goal state after:
y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 1 + y / x = (x + y) / x

y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 0 < x

y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 0 < x + y
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 (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 if x = 0 then if n = 0 then 1 else 0 else cexp ((starRingEnd ℂ) (log x) * n)

Tactic:
log_conj_eq_ite

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

Goal state before:
pp: θ : Angle
⊢ (2 • θ).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal

Tactic:
by
  nth_rw 1 [← coe_toReal θ]
  rw [← coe_nsmul, two_nsmul, ← two_mul, toReal_coe_eq_self_sub_two_pi_iff, Set.mem_Ioc]
  exact
    ⟨fun h => by linarith, fun h =>
      ⟨(div_lt_iff₀' (zero_lt_two' ℝ)).1 h, by linarith [pi_pos, toReal_le_pi θ]⟩⟩

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

Goal state before:
pp: θ : Angle
⊢ (↑π - θ).sign = θ.sign

Tactic:
simp [sign_antiperiodic.sub_eq']

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

Goal state before:
pp: y : ℝ
hy : 0 < y
⊢ Tendsto (fun x ↦ x ^ y) atTop atTop

Tactic:
rw [(atTop_basis' 0).tendsto_right_iff]
  intro b hb
  filter_upwards [eventually_ge_atTop 0, eventually_ge_atTop (b ^ (1 / y))] with x hx₀ hx
  simpa (disch := positivity) [Real.rpow_inv_le_iff_of_pos] using hx

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
rw [← Complex.ofReal_inj, Complex.ofReal_cpow (rpow_nonneg hx _),
      Complex.ofReal_cpow hx, Complex.ofReal_mul, Complex.cpow_mul, Complex.ofReal_cpow hx] <;>
    simp only [(Complex.ofReal_mul _ _).symm, (Complex.ofReal_log hx).symm, Complex.ofReal_im,
      neg_lt_zero, pi_pos, le_of_lt pi_pos]

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

Goal state before:
pp: x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ (x * y) ^ z = x ^ z * y ^ z

Tactic:
iterate 2 rw [Real.rpow_def_of_nonneg]; split_ifs with h_ifs <;> simp_all

Goal state after:
case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs✝ : ¬y = 0
h_ifs : ¬x = 0
⊢ rexp (log (x * y) * z) = rexp (log x * z) * y ^ z

case neg.hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ 0 ≤ x

case hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ 0 ≤ x * y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
y : ℝ
⊢ (x ^ y) ^ y⁻¹ = x ↔ y ≠ 0 ∨ x = 1

Tactic:
grind only [rpow_rpow_inv, rpow_zero]

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

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
hy : 0 < y
⊢ x ^ y < 1 ↔ x ^ y < 1 ^ y

Tactic:
Real.one_rpow

Goal state after:
x y : ℝ
hx : 0 ≤ x
hy : 0 < y
⊢ x ^ y < 1 ↔ x ^ y < 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inl
x : ℝ≥0∞
z : ℝ
H : z < 0
⊢ (x ^ z).toNNReal = x.toNNReal ^ z

Tactic:
cases x with
    | top => simp [H, ne_of_lt]
    | coe x =>
      by_cases hx : x = 0
      · simp [hx, H, ne_of_lt]
      · simp [← coe_rpow_of_ne_zero hx]

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

Goal state before:
pp: case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : p = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
simp [hp0]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ (lineMap y x) (1 - ⅟2) = midpoint R y x

Tactic:
one_sub_invOf_two,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ (lineMap y x) ⅟2 = midpoint R y x
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_2.inl.inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 < 0
hm1 : m 1 < 0
⊢ -m 0 • x = -m 1 • -y

Tactic:
linear_combination (norm := module) -hm

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_2.inl.inr.inr
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 < 0
hm1 : 0 < m 1
⊢ -m 0 • x = m 1 • y

Tactic:
linear_combination (norm := module) -hm

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_10
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
f : k →ᵃ[k] k
a b : k
⊢ ⇑f '' Set.uIcc a b = Set.uIcc (f a) (f b)

Tactic:
have : ⇑f = (fun x => x + f 0) ∘ fun x => x * (f 1 - f 0) := by
    ext x
    change f x = x • (f 1 -ᵥ f 0) +ᵥ f 0
    rw [← f.linearMap_vsub, ← f.linear.map_smul, ← f.map_vadd]
    simp only [vsub_eq_sub, add_zero, mul_one, vadd_eq_add, sub_zero, smul_eq_mul]
  rw [this, Set.image_comp]
  simp only [Set.image_add_const_uIcc, Set.image_mul_const_uIcc, Function.comp_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
⊢ SameRay R x y ∧ y ≠ 0 → ∃ r, 0 < r ∧ r • x = y

Tactic:
rintro ⟨hxy, hy⟩
    exact (exists_pos_left_iff_sameRay hx hy).2 hxy

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ x = r • y) ↔ SameRay R x y

Tactic:
SameRay.sameRay_comm

Goal state after:
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ x = r • y) ↔ SameRay R y x
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ x = r • y) ↔ SameRay R x y ∧ x ≠ 0

Tactic:
SameRay.sameRay_comm

Goal state after:
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ x = r • y) ↔ SameRay R y x ∧ x ≠ 0
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 ≤ r ∧ x = r • y) ↔ SameRay R x y

Tactic:
SameRay.sameRay_comm

Goal state after:
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 ≤ r ∧ x = r • y) ↔ SameRay R y x