mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r) = closedBall x r

Tactic:
refine Subset.antisymm closure_ball_subset_closedBall fun y hy => ?_
  have : ContinuousWithinAt (fun c : ℝ => c • (y - x) + x) (Ico 0 1) 1 := by fun_prop
  convert! this.mem_closure _ _
  · rw [one_smul, sub_add_cancel]
  · simp [closure_Ico zero_ne_one, zero_le_one]
  · rintro c ⟨hc0, hc1⟩
    rw [mem_ball, dist_eq_norm, add_sub_cancel_right, norm_smul, Real.norm_eq_abs,
      abs_of_nonneg hc0, mul_comm, ← mul_one r]
    rw [mem_closedBall, dist_eq_norm] at hy
    replace hr : 0 < r := ((norm_nonneg _).trans hy).lt_of_ne hr.symm
    apply mul_lt_mul' <;> assumption

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

Goal state before:
pp: θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
⊢ ¬s = 0

Tactic:
sin_eq_zero_iff,

Goal state after:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
⊢ ¬∃ n, ↑n * π = θ
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
γ' : Path y z
⊢ Continuous[_, inst✝¹] ((fun t ↦ if t ≤ 1 / 2 then γ.extend (2 * t) else γ'.extend (2 * t - 1)) ∘ Subtype.val)

Tactic:
by
    refine
      (Continuous.if_le ?_ ?_ continuous_id continuous_const (by simp)).comp
        continuous_subtype_val <;>
    fun_prop

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: case pos
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ γ' ⟨2 * ↑(σ t) - 1, ⋯⟩ = γ' (σ ⟨2 * ↑t, ⋯⟩)

pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ γ' ⟨2 * ↑(σ t) - 1, ⋯⟩ = γ (σ ⟨2 * ↑t - 1, ⋯⟩)

Tactic:
· refine congr_arg _ (Subtype.ext ?_)
    simp only [coe_symm_eq]
    ring

Goal state after:
case neg
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
h✝ : ¬↑(σ t) ≤ 1 / 2
h : ¬1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ γ' ⟨2 * ↑(σ t) - 1, ⋯⟩ = γ (σ ⟨2 * ↑t - 1, ⋯⟩)
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
t : Set X
f : T → X → Y
g : C(↑t, Y)
f_cont : ContinuousOn (Function.uncurry f) (univ ×ˢ t)
this : ∀ (x : T), ContinuousOn (f x) t
x : T
y : ↑t
| mkD (t.domRestrict (f x)) g

Tactic:
mkD_of_continuousOn (this x)

Goal state after:
X : Type u_2
Y : Type u_3
T : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace T
t : Set X
f : T → X → Y
g : C(↑t, Y)
f_cont : ContinuousOn (Function.uncurry f) (univ ×ˢ t)
this : ∀ (x : T), ContinuousOn (f x) t
x : T
y : ↑t
| { toFun := t.domRestrict (f x), continuous_toFun := ⋯ }
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
⊢ ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|

Tactic:
by
    rcases eq_or_ne p 0 with (rfl | hp)
    · simp
    have hx := norm_coe_mul p x p⁻¹
    rw [abs_inv, eq_inv_mul_iff_mul_eq₀ ((not_congr abs_eq_zero).mpr hp)] at hx
    rw [← hx, inv_mul_cancel₀ hp, this, ← abs_mul, mul_sub, mul_inv_cancel_left₀ hp, mul_comm p]

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

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k : ℕ
ha : Antitone fun n ↦ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i
n : ℕ
⊢ id n ≤ 2 * n

Tactic:
dsimp

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k : ℕ
ha : Antitone fun n ↦ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i
n : ℕ
⊢ n ≤ 2 * n
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : ↑I
h₁ : Continuous (IccExtend ⋯ f)
this : Icc (f ⟨0, ⋯⟩) (f ⟨1, ⋯⟩) ⊆ IccExtend ⋯ f '' Icc 0 1
⊢ ∃ a, f a = t

Tactic:
Icc.mk_zero,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : ↑I
h₁ : Continuous (IccExtend ⋯ f)
this : Icc (f 0) (f ⟨1, ⋯⟩) ⊆ IccExtend ⋯ f '' Icc 0 1
⊢ ∃ a, f a = t
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k : ℕ
hm : Monotone fun n ↦ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
n : ℕ
⊢ id n ≤ 2 * n + 1

Tactic:
dsimp

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k : ℕ
hm : Monotone fun n ↦ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
n : ℕ
⊢ n ≤ 2 * n + 1
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
hm : Monotone fun n ↦ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i
n : ℕ
⊢ id n ≤ 2 * n

Tactic:
dsimp

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
hm : Monotone fun n ↦ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i
n : ℕ
⊢ n ≤ 2 * n
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
ha : Antitone fun n ↦ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
n : ℕ
⊢ id n ≤ 2 * n + 1

Tactic:
dsimp

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
ha : Antitone fun n ↦ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
n : ℕ
⊢ n ≤ 2 * n + 1
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
⊢ p * 1 ≤ p * (↑(addOrderOf u) * (↑n / ↑(addOrderOf u)))

Tactic:
mul_div_cancel₀ _ hu,

Goal state after:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
⊢ p * 1 ≤ p * ↑n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp
θ ψ : ℝ
Hcos : sin ((θ + ψ) / 2) = 0 ∨ sin ((θ - ψ) / 2) = 0
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ

Tactic:
sin_eq_zero_iff,

Goal state after:
case mp
θ ψ : ℝ
Hcos : (∃ n, ↑n * π = (θ + ψ) / 2) ∨ sin ((θ - ψ) / 2) = 0
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: ⊢ ∀ ⦃x : ℂ⦄, x ∈ {z | z.im ∈ Ioo (-π) π} → cexp x ∈ slitPlane

Tactic:
by
    rintro ⟨x, y⟩ ⟨h₁ : -π < y, h₂ : y < π⟩
    simp [exp_mem_slitPlane, h₂.ne,
      (toIocMod_eq_self Real.two_pi_pos).mpr ⟨h₁, by simpa [two_mul] using h₂.le⟩]

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

Goal state before:
pp: x : ℂ
⊢ ((starRingEnd ℂ) x).arg = if x.arg = π then π else -x.arg

Tactic:
by
  simp_rw [arg_eq_pi_iff, arg, neg_im, conj_im, conj_re, norm_conj, neg_div, neg_neg,
    Real.arcsin_neg]
  rcases lt_trichotomy x.re 0 with (hr | hr | hr) <;>
    rcases lt_trichotomy x.im 0 with (hi | hi | hi)
  · simp [hr, hr.not_ge, hi.le, hi.ne, not_le.2 hi, add_comm]
  · simp [hr, hr.not_ge, hi]
  · simp [hr, hr.not_ge, hi.ne.symm, hi.le, not_le.2 hi, sub_eq_neg_add]
  · simp [hr]
  · simp [hr]
  · simp [hr]
  · simp [hr.le, hi.ne]
  · simp [hr.le, hr.le.not_gt]
  · simp [hr.le, hr.le.not_gt]

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

Goal state before:
pp: case inl
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = ↑ψ
⊢ ↑θ = ↑ψ

pp: case inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = -↑ψ
⊢ ↑θ = ↑ψ

Tactic:
· exact hc

Goal state after:
case inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = -↑ψ
⊢ ↑θ = ↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (↑(2 * θ.toReal)).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2

Tactic:
toReal_coe_eq_self_add_two_pi_iff,

Goal state after:
θ : Angle
⊢ 2 * θ.toReal ∈ Set.Ioc (-3 * π) (-π) ↔ θ.toReal ≤ -π / 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: r : ℝ
hr : 0 < r
θ : Real.Angle
⊢ ↑(↑r * (↑θ.cos + ↑θ.sin * I)).arg = θ

Tactic:
induction θ using Real.Angle.induction_on with | _ θ

Goal state after:
case h
r : ℝ
hr : 0 < r
θ : ℝ
⊢ ↑(↑r * (↑(↑θ).cos + ↑(↑θ).sin * I)).arg = ↑θ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h.h
x✝¹ x✝ : ℝ
k : ℤ
h : 2 * (x✝¹ + x✝) = 2 * (2 * (2⁻¹ * π) * ↑k + 2⁻¹ * π)
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹

Tactic:
mul_right_inj' (two_ne_zero' ℝ),

Goal state after:
case h.h
x✝¹ x✝ : ℝ
k : ℤ
h : x✝¹ + x✝ = 2 * (2⁻¹ * π) * ↑k + 2⁻¹ * π
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ ψ.tan = θ.tan⁻¹

Tactic:
exact tan_eq_inv_of_two_nsmul_add_two_nsmul_eq_pi h

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

Goal state before:
pp: case refine_2
z : ℂ
hre : z.re < 0
him : z.im = 0
this : arg =ᶠ[𝓝[{z | 0 ≤ z.im}] z] fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π
⊢ z.arg = Real.arcsin ((-z).im / ‖z‖) + π

Tactic:
rw [arg, if_neg hre.not_ge, if_pos him.ge]

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

Goal state before:
pp: x : ℝ
hx : x < 0
y : ℝ
this : Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I
⊢ (↑(rexp (log (-x) * y)) * (Complex.cos ↑(y * π) + Complex.sin ↑(y * π) * Complex.I)).re =
    rexp (log x * y) * cos (y * π)

Tactic:
← Complex.ofReal_cos,

Goal state after:
x : ℝ
hx : x < 0
y : ℝ
this : Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I
⊢ (↑(rexp (log (-x) * y)) * (↑(cos (y * π)) + Complex.sin ↑(y * π) * Complex.I)).re = rexp (log x * y) * cos (y * π)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ 0 ≤ if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)

Tactic:
split_ifs <;>
    simp only [zero_le_one, le_refl, le_of_lt (exp_pos _)]

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

Goal state before:
pp: a b : ℝ
h : a ≤ b
himp : b = 0 → a = 0
x : ℝ
hx : x ∈ Set.Icc 0 1
⊢ x ∈ {x | (fun x ↦ ‖x ^ b‖ ≤ ‖x ^ a‖) x}

Tactic:
simpa [Real.abs_rpow_of_nonneg hx.1, abs_of_nonneg hx.1]
     using Real.rpow_le_rpow_of_exponent_ge_of_imp hx.1 hx.2 h fun _ ↦ himp

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

Goal state before:
pp: k a b : ℝ
ha' : a < b
⊢ (fun t ↦ rexp (a * t) * t ^ k) =o[atTop] fun t ↦ rexp (b * t)

Tactic:
refine (isLittleO_of_tendsto (fun _ h ↦ (Real.exp_ne_zero _ h).elim) ?_)
  simp_rw [← div_mul_eq_mul_div₀, ← Real.exp_sub, ← sub_mul, ← neg_sub b a,
    mul_comm _ (_ ^ k)]
  exact tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero _ _ (sub_pos.mpr ha')

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

Goal state before:
pp: x✝ : ℝ≥0
w y✝ z y : ℝ
hy : 0 < y
x : ℝ≥0
⊢ (fun x ↦ x ^ y) ((fun x ↦ x ^ (1 / y)) x) = x

Tactic:
dsimp

Goal state after:
x✝ : ℝ≥0
w y✝ z y : ℝ
hy : 0 < y
x : ℝ≥0
⊢ (x ^ (1 / y)) ^ y = x
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hxy : x ≤ y
hx0 : x ≠ 0
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z

Tactic:
rcases eq_or_ne y 0 with (rfl | hy0)

Goal state after:
case inr.inl
x : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hx0 : x ≠ 0
hxy : x ≤ 0
⊢ (x * 0) ^ z = if (x = 0 ∧ 0 = ∞ ∨ x = ∞ ∧ 0 = 0) ∧ z < 0 then ∞ else x ^ z * 0 ^ z

case inr.inr
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hxy : x ≤ y
hx0 : x ≠ 0
hy0 : y ≠ 0
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x y : ℝ≥0∞
z : ℝ
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z

Tactic:
by
  rcases eq_or_ne z 0 with (rfl | hz); · simp
  replace hz := hz.lt_or_gt
  wlog hxy : x ≤ y
  · convert! this y x z hz (le_of_not_ge hxy) using 2 <;> simp only [mul_comm, and_comm, or_comm]
  rcases eq_or_ne x 0 with (rfl | hx0)
  · induction y <;> rcases hz with hz | hz <;> simp [*, hz.not_gt]
  rcases eq_or_ne y 0 with (rfl | hy0)
  · exact (hx0 (bot_unique hxy)).elim
  induction x
  · rcases hz with hz | hz <;> simp [hz, top_unique hxy]
  induction y
  · rw [ne_eq, coe_eq_zero] at hx0
    rcases hz with hz | hz <;> simp [*]
  simp only [*]
  norm_cast at *
  rw [← coe_rpow_of_ne_zero (mul_ne_zero hx0 hy0), NNReal.mul_rpow]
  norm_cast

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

Goal state before:
pp: x : ℝ≥0∞
y : ℝ
⊢ x⁻¹ ^ y = (x ^ y)⁻¹

Tactic:
by
  rcases eq_or_ne y 0 with (rfl | hy); · simp only [rpow_zero, inv_one]
  replace hy := hy.lt_or_gt
  rcases eq_or_ne x 0 with (rfl | h0); · cases hy <;> simp [*]
  rcases eq_or_ne x ⊤ with (rfl | h_top); · cases hy <;> simp [*]
  apply ENNReal.eq_inv_of_mul_eq_one_left
  rw [← mul_rpow_of_ne_zero (ENNReal.inv_ne_zero.2 h_top) h0, ENNReal.inv_mul_cancel h0 h_top,
    one_rpow]

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

Goal state before:
pp: y : ℝ
hy : 0 < y
x : ℝ≥0∞
⊢ (fun x ↦ x ^ y) ((fun x ↦ x ^ (1 / y)) x) = x

Tactic:
dsimp

Goal state after:
y : ℝ
hy : 0 < y
x : ℝ≥0∞
⊢ (x ^ (1 / y)) ^ y = x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr
x : ℝ
h : x < 0
⊢ √x = x ^ (1 / 2)

Tactic:
have : 1 / (2 : ℝ) * π = π / (2 : ℝ) := by ring
    rw [sqrt_eq_zero_of_nonpos h.le, rpow_def_of_neg h, this, cos_pi_div_two, mul_zero]

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) ⅟2 = midpoint R y x

Tactic:
midpoint

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 = (lineMap y x) ⅟2
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_2.inr.inr.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 : 0 < m 0
hm1 : 0 < m 1
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
refine Or.inr (Or.inr (Or.inr ⟨m 0, m 1, hm0, hm1, ?_⟩))

Goal state after:
case neg.refine_2.inr.inr.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 : 0 < m 0
hm1 : 0 < m 1
⊢ m 0 • x = m 1 • -y
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr
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
h : SameRay R x y
hx : x ≠ 0
hy : y ≠ 0
⊢ ∃ r, 0 ≤ r ∧ r • x = y

Tactic:
· exact (h.exists_pos_left hx hy).imp fun _ => And.imp_left le_of_lt

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
s : Set E
⊢ Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s

Tactic:
convex_iff_segment_subset,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
s : Set E
⊢ (∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → [x -[𝕜] y] ⊆ s) ↔
    ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : (↑s).Nonempty
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ : P
hp₂ : p₂ ∈ ↑s
p₃ : P
hp₃ : p₃ ∈ ↑s
p₄ : P
hp₄ : p₄ ∈ ↑s
⊢ (fun x1 x2 ↦ x1 -ᵥ x2) p₁ p₂ +ᵥ p₃ ∈ ↑s

Tactic:
rw [mem_coe]

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : (↑s).Nonempty
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ : P
hp₂ : p₂ ∈ ↑s
p₃ : P
hp₃ : p₃ ∈ ↑s
p₄ : P
hp₄ : p₄ ∈ ↑s
⊢ (fun x1 x2 ↦ x1 -ᵥ x2) p₁ p₂ +ᵥ p₃ ∈ s
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
v : V
⊢ v ∈ s.direction ↔ ∃ p₂ ∈ s, v = p -ᵥ p₂

Tactic:
by
  rw [← SetLike.mem_coe, coe_direction_eq_vsub_set_left hp]
  exact ⟨fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩, fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩⟩

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
⊢ Convex 𝕜 s ↔ s.OrdConnected

Tactic:
convex_iff_segment_subset,

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
⊢ (∀ ⦃x : 𝕜⦄, x ∈ s → ∀ ⦃y : 𝕜⦄, y ∈ s → [x -[𝕜] y] ⊆ s) ↔ s.OrdConnected
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
a : 𝕜
ha : s ⊆ a • Metric.closedBall 0 1
⊢ Bornology.IsVonNBounded 𝕜 s

Tactic:
exact ((isVonNBounded_closedBall 𝕜 E 1).image (a • (1 : E →L[𝕜] E))).subset ha

Goal state after:
Module: Mathlib.Topology.MetricSpace.Equicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
⊢ EquicontinuousAt F x₀ ↔ ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε

Tactic:
equicontinuousAt_iff_pair

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
⊢ (∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U) ↔
    ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
| vectorSpan k (p '' s)

Tactic:
vectorSpan_eq_span_vsub_set_right k (Set.mem_image_of_mem p hi),

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
| Submodule.span k ((fun x ↦ x -ᵥ p i) '' p '' s)
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case f
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
h : ∑ i ∈ s, w i = 0
b₁ b₂ : P
| fun x ↦ w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)

Tactic:
ext
      rw [← smul_sub, vsub_sub_vsub_cancel_left]

Goal state after:
case f
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
h : ∑ i ∈ s, w i = 0
b₁ b₂ : P
x✝ : ι
| w x✝ • (b₂ -ᵥ b₁)
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0
h1 : ∑ i ∈ s, w i = 1
i2 : ι
⊢ i2 ∈ s → w i2 • (p i2 -ᵥ p i) = 0

Tactic:
hi2

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
i : ι
his : i ∈ s
hwi : w i = 1
hw0 : ∀ i2 ∈ s, i2 ≠ i → w i2 = 0
h1 : ∑ i ∈ s, w i = 1
i2 : ι
hi2 : i2 ∈ s
⊢ w i2 • (p i2 -ᵥ p i) = 0
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x✝ x : E
⊢ 0 ≤ (fun u ↦ p u + q (x✝ - u)) x

Tactic:
dsimp

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x✝ x : E
⊢ 0 ≤ p x + q (x✝ - x)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
H : BddAbove (DFunLike.coe '' s)
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
⊢ p x ≤ (sSup s) x

Tactic:
dsimp

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
H : BddAbove (DFunLike.coe '' s)
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
⊢ p x ≤ (sSup s) x
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case refine_1
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
this : Nonempty ↑s
⊢ p x ≤ (sSup s) x

Tactic:
dsimp

Goal state after:
case refine_1
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
this : Nonempty ↑s
⊢ p x ≤ (sSup s) x
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case refine_2
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ upperBounds s
x : E
this : Nonempty ↑s
⊢ (sSup s) x ≤ p x

Tactic:
dsimp

Goal state after:
case refine_2
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ upperBounds s
x : E
this : Nonempty ↑s
⊢ (sSup s) x ≤ p x