mathlib-initiative/mathlib-tactics huggingface dataset:
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✝¹ : Ring R
inst✝ : Module R M
S T : Submodule R M
h : S = T
⊢ ∀ (x : M ⧸ S), ‖(S.quotEquivOfEq T h) x‖ = ‖x‖

Tactic:
subst h

Goal state after:
M : Type u_1
N : Type u_2
inst✝³ : SeminormedAddCommGroup M
inst✝² : SeminormedAddCommGroup N
R : Type u_3
inst✝¹ : Ring R
inst✝ : Module R M
S : Submodule R M
__spread✝⁻⁰ : (M ⧸ S) ≃ₗ[R] M ⧸ S := S.quotEquivOfEq S ⋯
⊢ ∀ (x : M ⧸ S), ‖(S.quotEquivOfEq S ⋯) x‖ = ‖x‖
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
x : Set E
⊢ (ediam (c • x)).toReal = ‖c‖ * (ediam x).toReal

Tactic:
ediam_smul₀,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
x : Set E
⊢ (‖c‖₊ • ediam x).toReal = ‖c‖ * (ediam x).toReal
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case pos
R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n ↦ x ^ n
⊢ ‖∑' (n : ℕ), x ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Tactic:
rw [hx.tsum_eq_zero_add]

Goal state after:
case pos
R : Type u_4
inst✝ : NormedRing R
x : R
h : ‖x‖ < 1
hx : Summable fun n ↦ x ^ n
⊢ ‖x ^ 0 + ∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: z : ℂ
⊢ sin z = 0 ↔ sin z = 0 ∨ sin z = 0

Tactic:
or_self

Goal state after:
z : ℂ
⊢ sin z = 0 ↔ sin z = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: z : ℂ
⊢ cos z = 0 ↔ cos z = 0 ∨ cos z = 0

Tactic:
or_self

Goal state after:
z : ℂ
⊢ cos z = 0 ↔ cos z = 0
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
a b : E
⊢ Metric.ball (a +ᵥ b) (ε + δ) = Metric.ball (a + b) (ε + δ)

Tactic:
vadd_eq_add

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
a b : E
⊢ Metric.ball (a + b) (ε + δ) = Metric.ball (a + b) (ε + δ)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.ball (a +ᵥ b) (ε + δ) = Metric.ball (a + b) (ε + δ)

Tactic:
vadd_eq_add

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.ball (a + b) (ε + δ) = Metric.ball (a + b) (ε + δ)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
⊢ ∃ a, ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i

Tactic:
let P : Polynomial ℕ := (ascPochhammer ℕ k).comp (Polynomial.X + C 1)

Goal state after:
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
P : ℕ[X] := (ascPochhammer ℕ k).comp (X + C 1)
⊢ ∃ a, ∀ (n : ℕ), (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, a i * n ^ i
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
⊢ c • closedBall 0 1 = closedBall 0 ‖c‖

Tactic:
_root_.smul_closedBall _ _ zero_le_one,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
⊢ closedBall (c • 0) (‖c‖ * 1) = closedBall 0 ‖c‖
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ⤳ y
hx : x ∈ F
hy : y ∈ F
⊢ JoinedIn F x y

Tactic:
by
  refine ⟨⟨⟨Set.piecewise {1} (const I y) (const I x), ?_⟩, by simp, by simp⟩, fun t ↦ ?_⟩
  · exact isClosed_singleton.continuous_piecewise_of_specializes continuous_const continuous_const
      fun _ ↦ h
  · simp only [Path.coe_mk_mk, piecewise]
    split_ifs <;> assumption

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
hU : IsOpen[inst✝¹] U
hKU : MapsTo (⇑g ∘ ⇑f) K U
L : Set Y
hKL : L ∈ 𝓝ˢ (⇑f '' K)
hLc : IsCompact L
hLU : MapsTo (⇑g) L U
⊢ ∀ᶠ (a : C(X, Y) × C(Y, Z)) in 𝓝 (f, g), MapsTo (⇑(a.2.comp a.1)) K U

Tactic:
rw [← subset_interior_iff_mem_nhdsSet, ← mapsTo_iff_image_subset] at hKL

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
hU : IsOpen[inst✝¹] U
hKU : MapsTo (⇑g ∘ ⇑f) K U
L : Set Y
hKL : MapsTo (⇑f) K (interior L)
hLc : IsCompact L
hLU : MapsTo (⇑g) L U
⊢ ∀ᶠ (a : C(X, Y) × C(Y, Z)) in 𝓝 (f, g), MapsTo (⇑(a.2.comp a.1)) K U
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
⊢ IsPathConnected F ↔ IsPathConnected {x | x ∈ F}

Tactic:
ofPred_mem_eq

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
⊢ IsPathConnected F ↔ IsPathConnected F
Module: Mathlib.Topology.Path

Goal state before:
pp: case pos
ι : Type u_3
χ : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : ↑I
i : ι
h✝ : ↑t ≤ 1 / 2
⊢ (Path.pi γ₀).extend (2 * ↑t) i = (γ₀ i).extend (2 * ↑t)

pp: case neg
ι : Type u_3
χ : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : ↑I
i : ι
h✝ : ¬↑t ≤ 1 / 2
⊢ (Path.pi γ₁).extend (2 * ↑t - 1) i = (γ₁ i).extend (2 * ↑t - 1)

Tactic:
· rfl

Goal state after:
case neg
ι : Type u_3
χ : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : ↑I
i : ι
h✝ : ¬↑t ≤ 1 / 2
⊢ (Path.pi γ₁).extend (2 * ↑t - 1) i = (γ₁ i).extend (2 * ↑t - 1)
Module: Mathlib.Topology.Path

Goal state before:
pp: case neg
ι : Type u_3
χ : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (χ i)
as bs cs : (i : ι) → χ i
γ₀ : (i : ι) → Path (as i) (bs i)
γ₁ : (i : ι) → Path (bs i) (cs i)
t : ↑I
i : ι
h✝ : ¬↑t ≤ 1 / 2
⊢ (Path.pi γ₁).extend (2 * ↑t - 1) i = (γ₁ i).extend (2 * ↑t - 1)

Tactic:
· rfl

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: case neg
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : t₀ ≤ ↑1
h₂ : ¬↑1 ≤ t₁
⊢ γ.extend t₁ = γ.extend t₁

pp: case pos
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : ¬t₀ ≤ ↑1
h₃ : t₀ ≤ t₁
⊢ γ.extend t₀ = γ.extend t₁

pp: case neg
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : ¬t₀ ≤ ↑1
h₃ : ¬t₀ ≤ t₁
⊢ γ.extend t₁ = γ.extend t₁

Tactic:
· rfl

Goal state after:
case pos
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : ¬t₀ ≤ ↑1
h₃ : t₀ ≤ t₁
⊢ γ.extend t₀ = γ.extend t₁

case neg
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : ¬t₀ ≤ ↑1
h₃ : ¬t₀ ≤ t₁
⊢ γ.extend t₁ = γ.extend t₁
Module: Mathlib.Topology.Path

Goal state before:
pp: case neg
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : ¬t₀ ≤ ↑1
h₃ : ¬t₀ ≤ t₁
⊢ γ.extend t₁ = γ.extend t₁

Tactic:
· rfl

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

Goal state before:
pp: case hf
α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f₁ f₂ : α → K
g : α → R
t : R
l : Filter α
hmul : Tendsto (fun x ↦ f₁ x • g x) l (𝓝 t)
hf₁ : Tendsto f₁ l (cobounded K)
hbdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f₁ x - f₂ x‖
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ (norm ∘ fun x ↦ ‖f₁ x - f₂ x‖) x

Tactic:
simpa using hbdd

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

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

Tactic:
Nat.cast_ofNat,

Goal state after:
ψ θ : Angle
⊢ 2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
⊢ log ↑n = n.factorization.sum fun p t ↦ ↑t * log ↑p

Tactic:
simp only [← log_pow, ← Nat.cast_pow]

Goal state after:
case inr
n : ℕ
hn : n ≠ 0
⊢ log ↑n = n.factorization.sum fun p t ↦ log ↑(p ^ t)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: a b : ℝ
n : ℕ
ha : a ≠ 0
⊢ (fun x ↦ x ^ n / (a * rexp x + b)) ∘ log =ᶠ[atTop] fun x ↦ log x ^ n / (a * x + b)

Tactic:
by
    filter_upwards [eventually_gt_atTop (0 : ℝ)] with x hx using by simp [exp_log hx]

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

Goal state before:
pp: case inr.inl
z : ℂ
hre : z.re = 0
⊢ (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im

pp: case inr.inr
z : ℂ
hre : 0 < z.re
⊢ (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im

Tactic:
· simp [hre]

Goal state after:
case inr.inr
z : ℂ
hre : 0 < z.re
⊢ (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im
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) * n) else -(log x * n))) =
    if x.arg = π then
      (if x = 0 then if n = 0 then (starRingEnd ℂ) 1 else (starRingEnd ℂ) 0
        else (starRingEnd ℂ) (cexp (log x * (starRingEnd ℂ) n)))⁻¹
    else (if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n))⁻¹

Tactic:
apply_ite exp,

Goal state after:
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0
    else if x.arg = π then cexp (-((starRingEnd ℂ) (log x) * n)) else cexp (-(log x * n))) =
    if x.arg = π then
      (if x = 0 then if n = 0 then (starRingEnd ℂ) 1 else (starRingEnd ℂ) 0
        else (starRingEnd ℂ) (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: ⊢ (↑π).cos = -1

Tactic:
by rw [cos_coe, Real.cos_pi]

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

Goal state before:
pp: case pos
x n : ℂ
h : x.arg = π
⊢ (x ^ n)⁻¹ = (x ^ n)⁻¹

pp: case neg
x n : ℂ
h : ¬x.arg = π
⊢ (x ^ n)⁻¹ = x⁻¹ ^ n

Tactic:
· rfl

Goal state after:
case neg
x n : ℂ
h : ¬x.arg = π
⊢ (x ^ n)⁻¹ = x⁻¹ ^ n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inl
θ : Angle
⊢ |θ.sin| = |θ.sin|

pp: case inr
ψ : Angle
⊢ |(ψ + ↑π).sin| = |ψ.sin|

Tactic:
· rfl

Goal state after:
case inr
ψ : Angle
⊢ |(ψ + ↑π).sin| = |ψ.sin|
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case neg
x n : ℂ
h : ¬x.arg = π
⊢ (x ^ n)⁻¹ = x⁻¹ ^ n

Tactic:
· rw [inv_cpow _ _ h]

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

Goal state before:
pp: case inl
θ : Angle
⊢ |θ.cos| = |θ.cos|

pp: case inr
ψ : Angle
⊢ |(ψ + ↑π).cos| = |ψ.cos|

Tactic:
· rfl

Goal state after:
case inr
ψ : Angle
⊢ |(ψ + ↑π).cos| = |ψ.cos|
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ (↑z.arg).toReal = z.arg

Tactic:
by
  rw [Real.Angle.toReal_coe_eq_self_iff_mem_Ioc]
  exact arg_mem_Ioc _

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

Goal state before:
pp: x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ (x * y).arg = x.arg + y.arg ↔ x.arg + y.arg ∈ Ioc (-π) π

Tactic:
by
  rw [← arg_coe_angle_toReal_eq_arg, arg_mul_coe_angle hx₀ hy₀, ← Real.Angle.coe_add,
      Real.Angle.toReal_coe_eq_self_iff_mem_Ioc]

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

Goal state before:
pp: case inl
θ : Angle
⊢ θ.tan = θ.tan

pp: case inr
ψ : Angle
⊢ (ψ + ↑π).tan = ψ.tan

Tactic:
· rfl

Goal state after:
case inr
ψ : Angle
⊢ (ψ + ↑π).tan = ψ.tan
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case pos
x a : ℝ
hyp : (0 ^ ↑x).re = a
h : x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
subst h

Goal state after:
case pos
a : ℝ
hyp : (0 ^ ↑0).re = a
⊢ 0 ≠ 0 ∧ a = 0 ∨ 0 = 0 ∧ a = 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
⊢ x ^ (log x)⁻¹ = rexp 1

Tactic:
by
  rw [rpow_def_of_pos hx₀, mul_inv_cancel₀]
  exact log_ne_zero.2 ⟨hx₀.ne', hx₁, by bound⟩

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

Goal state before:
pp: s b : ℝ
hb : 0 < b
⊢ Tendsto (fun x ↦ x ^ s * rexp (-b * x)) atTop (𝓝 0)

Tactic:
refine (tendsto_exp_mul_div_rpow_atTop s b hb).inv_tendsto_atTop.congr' ?_

Goal state after:
s b : ℝ
hb : 0 < b
⊢ (fun x ↦ rexp (b * x) / x ^ s)⁻¹ =ᶠ[atTop] fun x ↦ x ^ s * rexp (-b * x)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: z w : ℂ
h : z = 0 → w.re = 0 → w = 0
⊢ ‖z ^ w‖ = ‖z‖ ^ w.re / rexp (z.arg * w.im)

Tactic:
by
  rcases ne_or_eq z 0 with (hz | rfl) <;> [exact norm_cpow_of_ne_zero hz w; rw [norm_zero]]
  rcases eq_or_ne w.re 0 with hw | hw
  · simp [h rfl hw]
  · rw [Real.zero_rpow hw, zero_div, zero_cpow, norm_zero]
    exact ne_of_apply_ne re hw

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

Goal state before:
pp: case hgf
a : ℝ
ha : 0 < a
b : ℝ
⊢ ∀ᶠ (x : ℝ) in atTop, x ^ b = 0 → rexp (-a * x) = 0

pp: case a
a : ℝ
ha : 0 < a
b : ℝ
⊢ Tendsto (fun x ↦ rexp (-a * x) / x ^ b) atTop (𝓝 0)

Tactic:
· refine (eventually_gt_atTop 0).mono fun t ht h => ?_
    rw [rpow_eq_zero_iff_of_nonneg ht.le] at h
    exact (ht.ne' h.1).elim

Goal state after:
case a
a : ℝ
ha : 0 < a
b : ℝ
⊢ Tendsto (fun x ↦ rexp (-a * x) / x ^ b) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ ↑(x ^ (y + ↑n)) = ↑(x ^ y * x ^ n)

Tactic:
exact Real.rpow_add_natCast (mod_cast hx) _ _

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

Goal state before:
pp: case inl
x z : ℝ
h : 0 ≤ x
h₂ : 0 ≤ z
h₁ : x ≤ x
⊢ x ^ z ≤ x ^ z

pp: case inr
x y z : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₂ : 0 ≤ z
h₁' : x < y
⊢ x ^ z ≤ y ^ z

Tactic:
· rfl

Goal state after:
case inr
x y z : ℝ
h : 0 ≤ x
h₁ : x ≤ y
h₂ : 0 ≤ z
h₁' : x < y
⊢ x ^ z ≤ y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ i ∈ l, 0 ≤ f i
r : ℝ
⊢ (List.map (fun x ↦ f x ^ r) l).prod = (List.map ((fun x ↦ x ^ r) ∘ f) l).prod

pp: ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ i ∈ l, 0 ≤ f i
r : ℝ
⊢ ∀ x ∈ List.map f l, 0 ≤ x

Tactic:
· rfl

Goal state after:
ι : Type u_1
l : List ι
f : ι → ℝ
hl : ∀ i ∈ l, 0 ≤ f i
r : ℝ
⊢ ∀ x ∈ List.map f l, 0 ≤ x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: x q : ℝ
h : x ≠ 0 ∨ 0 ≤ q
⊢ ContinuousAt (fun x ↦ x ^ q) x

Tactic:
by
  rw [le_iff_lt_or_eq, ← or_assoc] at h
  obtain h | rfl := h
  · exact (continuousAt_rpow (x, q) h).comp₂ continuousAt_id continuousAt_const
  · simp_rw [rpow_zero]; exact continuousAt_const

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

Goal state before:
pp: x y z : ℝ
hx : 1 < x
⊢ ¬z ≤ y ↔ y < z

Tactic:
lt_iff_not_ge

Goal state after:
x y z : ℝ
hx : 1 < x
⊢ ¬z ≤ y ↔ ¬z ≤ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case inl
z w : ℂ
h₂ : 0 < (z, w).2.re
h₁ : 0 < (z, w).1.re ∨ (z, w).1.im ≠ 0
⊢ ContinuousAt (fun x ↦ x.1 ^ x.2) (z, w)

pp: case inr
w : ℂ
h₂ : 0 < (0, w).2.re
⊢ ContinuousAt (fun x ↦ x.1 ^ x.2) (0, w)

Tactic:
exacts [continuousAt_cpow h₁, continuousAt_cpow_zero_of_re_pos h₂]

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

Goal state before:
pp: x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
⊢ ¬y ≤ z ↔ z < y

Tactic:
lt_iff_not_ge

Goal state after:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
⊢ ¬y ≤ z ↔ ¬y ≤ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case top
n : ℕ
⊢ ∞ ^ ↑n = ∞ ^ n

Tactic:
cases n <;> simp [top_rpow_of_pos (Nat.cast_add_one_pos _), top_pow (Nat.succ_ne_zero _)]

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

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

Tactic:
cases x
    · simp [H, ne_of_gt]
    simp [← coe_rpow_of_nonneg _ (le_of_lt H)]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ midpoint R (x + y) (x - y) = x

Tactic:
rw [midpoint_comm]; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inl
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
r : R
hr : r < 0
⊢ 0 = 0

pp: case inr.inl
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
x : M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
r : R
hr : r < 0
h₀ : r • x = 0
⊢ x = 0

pp: case inr.inr
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
x : M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • r • x
⊢ x = 0

Tactic:
· rfl

Goal state after:
case inr.inl
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
x : M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
r : R
hr : r < 0
h₀ : r • x = 0
⊢ x = 0

case inr.inr
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
x : M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
r : R
hr : r < 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • r • x
⊢ x = 0
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inl
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₂ : M
⊢ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ 0 = a • (0 + v₂) ∧ v₂ = b • (0 + v₂)

Tactic:
use 0, 1

Goal state after:
case h
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₂ : M
⊢ 0 ≤ 0 ∧ 0 ≤ 1 ∧ 0 + 1 = 1 ∧ 0 = 0 • (0 + v₂) ∧ v₂ = 1 • (0 + v₂)
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
⊢ (a / (a + b)) • y + (b / (a + b)) • z ∈ openSegment 𝕜 y z

Tactic:
have hab : 0 < a + b := add_pos' ha hb

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 0 < a + b
⊢ (a / (a + b)) • y + (b / (a + b)) • z ∈ openSegment 𝕜 y z
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
S : AffineSpace V P
ι : Sort u_4
s : ι → AffineSubspace k P
p : P
⊢ p ∈ sInf (range s) ↔ ∀ (i : ι), p ∈ s i

Tactic:
mem_sInf_iff,

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
ι : Sort u_4
s : ι → AffineSubspace k P
p : P
⊢ (∀ s_1 ∈ range s, p ∈ s_1) ↔ ∀ (i : ι), p ∈ s i
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: case e'_6
R : Type u_5
inst✝⁹ : CommSemiring R
A : Type u_6
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
M : Type u_7
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module A M
inst✝⁴ : Module R M
inst✝³ : IsScalarTower R A M
inst✝² : PartialOrder R
inst✝¹ : PartialOrder A
inst✝ : FaithfulSMul R A
s : Set M
halg : Ici 0 ⊆ ⇑(algebraMap R A) '' Ici 0
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : R
hc1 : c ∈ Ici 0
hc2 : (algebraMap R A) c = a
d : R
hd1 : d ∈ Ici 0
hd2 : (algebraMap R A) d = b
⊢ b • v = d • v

Tactic:
rw [← hd2, algebraMap_smul]

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_6
ι : Type u_7
E : ι → Type u_8
inst✝³ : NormedDivisionRing 𝕜
inst✝² : (i : ι) → AddCommGroup (E i)
inst✝¹ : (i : ι) → Module 𝕜 (E i)
inst✝ : (i : ι) → TopologicalSpace (E i)
S : Set ((i : ι) → E i)
⊢ (∀ (i : ι), Tendsto (fun x ↦ (fun x_1 ↦ eval i (x • x_1)) '' S) (𝓝 0) (𝓝 (0 i)).smallSets) ↔
    ∀ (i : ι), Tendsto (fun x ↦ (fun x_1 ↦ x • eval i x_1) '' S) (𝓝 0) (𝓝 0).smallSets

Tactic:
eval,

Goal state after:
𝕜 : Type u_6
ι : Type u_7
E : ι → Type u_8
inst✝³ : NormedDivisionRing 𝕜
inst✝² : (i : ι) → AddCommGroup (E i)
inst✝¹ : (i : ι) → Module 𝕜 (E i)
inst✝ : (i : ι) → TopologicalSpace (E i)
S : Set ((i : ι) → E i)
⊢ (∀ (i : ι), Tendsto (fun x ↦ (fun a ↦ (x • a) i) '' S) (𝓝 0) (𝓝 (0 i)).smallSets) ↔
    ∀ (i : ι), Tendsto (fun x ↦ (fun a ↦ x • a i) '' S) (𝓝 0) (𝓝 0).smallSets
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s : Set E
⊢ IsVonNBounded 𝕜 (s + s) ↔ IsVonNBounded 𝕜 s

Tactic:
by
  rcases s.eq_empty_or_nonempty with rfl | hs <;> simp [isVonNBounded_add_of_nonempty, *]

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : ∀ U ∈ 𝓝 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h : ∃ x, 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁵, non_trivial := h }
U : Set E
hU : U ∈ 𝓝 0
⊢ Absorbs 𝕜 U s

Tactic:
have h : Filter.Tendsto (fun x : E × E => x.fst + x.snd) (𝓝 0) (𝓝 0) :=
      continuous_add.tendsto' _ _ (zero_add _)

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : UniformSpace E
inst✝¹ : IsUniformAddGroup E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : ∀ U ∈ 𝓝 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, y +ᵥ U
h✝ : ∃ x, 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁵, non_trivial := h✝ }
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x ↦ x.1 + x.2) (𝓝 0) (𝓝 0)
⊢ Absorbs 𝕜 U s