mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
⊢ ‖c‖₊ • ediam s ≤ ediam (c • s)

Tactic:
have := (lipschitzWith_smul c⁻¹).ediam_image_le (c • s)

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
this : ediam ((fun x ↦ c⁻¹ • x) '' (c • s)) ≤ ↑‖c⁻¹‖₊ * ediam (c • s)
⊢ ‖c‖₊ • ediam s ≤ ediam (c • s)
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
⊢ interior (closedBall x 0) = ball x 0

Tactic:
rw [closedBall_zero, ball_zero, interior_singleton]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
⊢ ∀ᶠ (r : 𝕜) in 𝓝 0, {x} + r • s ⊆ u

Tactic:
obtain ⟨ε, εpos, hε⟩ : ∃ ε : ℝ, 0 < ε ∧ closedBall x ε ⊆ u := nhds_basis_closedBall.mem_iff.1 hu

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
⊢ ∀ᶠ (r : 𝕜) in 𝓝 0, {x} + r • s ⊆ u
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 6) ^ 2 = 3 / 4

Tactic:
rw [cos_pi_div_six, div_pow, sq_sqrt] <;> norm_num

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

Goal state before:
pp: c : ℝ := cos (π / 5)
⊢ 4 * (c * c) + -2 * c + -1 = 0

Tactic:
← sq,

Goal state after:
c : ℝ := cos (π / 5)
⊢ 4 * c ^ 2 + -2 * c + -1 = 0
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
h : dist x z < ε + δ
⊢ (ε + δ) / (ε + δ) = 1

Tactic:
div_self (add_pos_of_pos_of_nonneg hε hδ).ne'

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
h : dist x z < ε + δ
⊢ 1 = 1
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case e'_5
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‖
n : ℕ
⊢ ↑((n + (k + 1)).choose (k + 1)) * r ^ n =
    ∑ k_1 ∈ Finset.range (n + 1), ↑((k_1 + k).choose k) * r ^ k_1 * r ^ (n - k_1)

Tactic:
have : ∑ i ∈ Finset.range (n + 1), ↑((i + k).choose k) * r ^ i * r ^ (n - i) =
            ∑ i ∈ Finset.range (n + 1), ↑((i + k).choose k) * r ^ n := by
          apply Finset.sum_congr rfl (fun i hi ↦ ?_)
          simp only [Finset.mem_range] at hi
          rw [mul_assoc, ← pow_add, show i + (n - i) = n by lia]

Goal state after:
case e'_5
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‖
n : ℕ
this :
  ∑ i ∈ Finset.range (n + 1), ↑((i + k).choose k) * r ^ i * r ^ (n - i) =
    ∑ i ∈ Finset.range (n + 1), ↑((i + k).choose k) * r ^ n
⊢ ↑((n + (k + 1)).choose (k + 1)) * r ^ n =
    ∑ k_1 ∈ Finset.range (n + 1), ↑((k_1 + k).choose k) * r ^ k_1 * r ^ (n - k_1)
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:
hU

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
⊢ 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.Analysis.SpecificLimits.Normed

Goal state before:
pp: case neg
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
⊢ Summable f

Tactic:
refine .of_norm_bounded_eventually_nat summable_zero ?_
    filter_upwards [h] with _ hn
    by_contra! h
    exact not_lt.mpr (norm_nonneg _) (lt_of_le_of_lt hn <| mul_neg_of_neg_of_pos hr₀ h)

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case right
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn F x = F
⊢ ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y

Tactic:
intro y y_in

Goal state after:
case right
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn F x = F
y : X
y_in : y ∈ F
⊢ JoinedIn F x y
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:
hU

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
⊢ MapsTo (⇑f) K U → ∀ᶠ (a : C(X, Y)) in (𝓝 f).lift' closure, MapsTo (⇑(id a)) K U
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
⊢ ∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ

Tactic:
cases p using snocCases with

Goal state after:
case snoc
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin n → X
x : X
hp : ∀ (i : Fin (n + 1)), snoc p x i ∈ s
⊢ ∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), snoc p x i ∈ range ⇑γ
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case mpr
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 : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i ↦ restrict s (F i)) l (𝓝 (f s a))
h :
  ∀ (s₁ : Set X) (hs₁ : IsCompact s₁) (s₂ : Set X) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    (f s₁ hs₁) ⟨x, hxs₁⟩ = (f s₂ hs₂) ⟨x, hxs₂⟩
⊢ ∀ (K : Set X),
    IsCompact K →
      Tendsto (fun i ↦ restrict K (F i)) l
        (𝓝 (restrict K (liftCover' (fun s ↦ ∀ ⦃f : Filter X⦄ [f.NeBot], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f) f h ⋯)))

Tactic:
intro s hs

Goal state after:
case mpr
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 : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i ↦ restrict s (F i)) l (𝓝 (f s a))
h :
  ∀ (s₁ : Set X) (hs₁ : IsCompact s₁) (s₂ : Set X) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    (f s₁ hs₁) ⟨x, hxs₁⟩ = (f s₂ hs₂) ⟨x, hxs₂⟩
s : Set X
hs : IsCompact s
⊢ Tendsto (fun i ↦ restrict s (F i)) l
    (𝓝 (restrict s (liftCover' (fun s ↦ ∀ ⦃f : Filter X⦄ [f.NeBot], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f) f h ⋯)))
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr.left
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
⊢ -(1 / 2) ≤ p⁻¹ * x

Tactic:
rwa [le_inv_mul_iff₀ hp, mul_neg, ← mul_div_assoc, mul_one]

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
x : ↑I
⊢ (γ.truncate 0 1) x = (γ.cast ⋯ ⋯) x

Tactic:
rw [cast_coe]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
x : ↑I
⊢ (γ.truncate 0 1) x = γ x
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
x : ↑I
⊢ (γ.truncate 0 1) x = γ x

Tactic:
have : ↑x ∈ (Icc 0 1 : Set ℝ) := x.2

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
x : ↑I
this : ↑x ∈ Icc 0 1
⊢ (γ.truncate 0 1) x = γ x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ arcsin (-x) = -arcsin x

Tactic:
by
  rcases le_total x (-1) with hx₁ | hx₁
  · rw [arcsin_of_le_neg_one hx₁, neg_neg, arcsin_of_one_le (le_neg.2 hx₁)]
  rcases le_total 1 x with hx₂ | hx₂
  · rw [arcsin_of_one_le hx₂, arcsin_of_le_neg_one (neg_le_neg hx₂)]
  refine arcsin_eq_of_sin_eq ?_ ?_
  · rw [sin_neg, sin_arcsin hx₁ hx₂]
  · exact ⟨neg_le_neg (arcsin_le_pi_div_two _), neg_le.2 (neg_pi_div_two_le_arcsin _)⟩

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

Goal state before:
pp: x : ℝ
⊢ π / 2 - arcsin x ≤ π / 4 ↔ √2 / 2 ≤ x

Tactic:
← pi_div_four_le_arcsin

Goal state after:
x : ℝ
⊢ π / 2 - arcsin x ≤ π / 4 ↔ π / 4 ≤ arcsin x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

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

Tactic:
ofReal_im,

Goal state after:
x : ℝ
hx : 0 ≤ x
⊢ 0 = (log ↑x).im
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
hx : 0 ≤ x.im
x✝ : ∃ n, x = ↑n * (2 * ↑π * I)
n : ℤ
hn : x = ↑n * (2 * ↑π * I)
this : 0 ≤ ↑n * (2 * π)
⊢ 0 ≤ n

Tactic:
exact_mod_cast nonneg_of_mul_nonneg_left this (by positivity)

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

Goal state before:
pp: z : ℂ
⊢ 0 ≤ z.re ∨ False ↔ 0 ≤ z.re

Tactic:
or_false

Goal state after:
z : ℂ
⊢ 0 ≤ z.re ↔ 0 ≤ z.re
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr
z : ℂ
hz : z ≠ 0
⊢ 0 < z.re ∨ False ↔ 0 < z.re

Tactic:
or_false

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

Goal state before:
pp: θ : ℝ
⊢ (↑θ).toReal = θ ↔ θ ∈ Set.Ioc (-π) π

Tactic:
toReal_coe_eq_self_iff,

Goal state after:
θ : ℝ
⊢ -π < θ ∧ θ ≤ π ↔ θ ∈ Set.Ioc (-π) π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: n : ℕ
h : n ≠ 0
θ : Angle
h' : 0 < ↑n
⊢ (↑(↑n * θ.toReal)).toReal = ↑n * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / ↑n) (π / ↑n)

Tactic:
toReal_coe_eq_self_iff,

Goal state after:
n : ℕ
h : n ≠ 0
θ : Angle
h' : 0 < ↑n
⊢ -π < ↑n * θ.toReal ∧ ↑n * θ.toReal ≤ π ↔ θ.toReal ∈ Set.Ioc (-π / ↑n) (π / ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : ℝ
k : ℤ
⊢ (↑(θ - 2 * ↑k * π)).toReal = θ - 2 * ↑k * π ↔ θ ∈ Set.Ioc ((2 * ↑k - 1) * π) ((2 * ↑k + 1) * π)

Tactic:
toReal_coe_eq_self_iff,

Goal state after:
θ : ℝ
k : ℤ
⊢ -π < θ - 2 * ↑k * π ∧ θ - 2 * ↑k * π ≤ π ↔ θ ∈ Set.Ioc ((2 * ↑k - 1) * π) ((2 * ↑k + 1) * π)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ z ∈ slitPlane ↔ z.arg ≠ π ∧ z ≠ 0

Tactic:
by
  simp only [mem_slitPlane_iff_not_le_zero, le_iff_lt_or_eq, ne_eq, arg_eq_pi_iff_lt_zero, not_or]

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

Goal state before:
pp: case inr
θ : Angle
h : θ ≠ ↑π
⊢ θ.toReal ∈ Set.Ioo 0 π ↔ θ.sign = 1

Tactic:
simp only [Set.mem_Ioo, ← sign_toReal h, sign_eq_one_iff, and_iff_left_iff_imp]
    exact fun _ ↦ (toReal_le_pi θ).lt_of_ne (toReal_eq_pi_iff.not.2 h)

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

Goal state before:
pp: case neg
x : ℂ
h : x ≠ 0
ha : Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z ↦ ↑z.arg + ↑π
hs : x.re ≤ 0 ∧ x.im = 0
⊢ 0 < (-x).re

Tactic:
neg_re,

Goal state after:
case neg
x : ℂ
h : x ≠ 0
ha : Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z ↦ ↑z.arg + ↑π
hs : x.re ≤ 0 ∧ x.im = 0
⊢ 0 < -x.re
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case h₁
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ -π < (↑(Real.log x * y)).im

Tactic:
ofReal_im,

Goal state after:
case h₁
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ -π < 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
by
  ext; exact Real.rpow_add_natCast' (mod_cast x.2) h

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

Goal state before:
pp: x z : ℝ
hx1 : 0 ≤ x
hx2 : x < 1
hz : 0 < z
⊢ x ^ z < 1

Tactic:
← one_rpow z

Goal state after:
x z : ℝ
hx1 : 0 ≤ x
hx2 : x < 1
hz : 0 < z
⊢ x ^ z < 1 ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x z : ℝ
hx1 : 0 ≤ x
hx2 : x ≤ 1
hz : 0 ≤ z
⊢ x ^ z ≤ 1

Tactic:
← one_rpow z

Goal state after:
x z : ℝ
hx1 : 0 ≤ x
hx2 : x ≤ 1
hz : 0 ≤ z
⊢ x ^ z ≤ 1 ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x z : ℝ
hx : 1 ≤ x
hz : z ≤ 0
⊢ x ^ z ≤ 1

Tactic:
convert! rpow_le_rpow_of_exponent_le hx hz

Goal state after:
x z : ℝ
hx : 1 ≤ x
hz : z ≤ 0
⊢ 1 = x ^ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x z : ℝ
hx : 1 < x
hz : 0 < z
⊢ 1 < x ^ z

Tactic:
← one_rpow z

Goal state after:
x z : ℝ
hx : 1 < x
hz : 0 < z
⊢ 1 ^ z < x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x z : ℝ
hx : 1 ≤ x
hz : 0 ≤ z
⊢ 1 ≤ x ^ z

Tactic:
← one_rpow z

Goal state after:
x z : ℝ
hx : 1 ≤ x
hz : 0 ≤ z
⊢ 1 ^ z ≤ x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case inr.inr.hf
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p ↦ (-↑p.1, p.2)) (x, y)
⊢ 0 < (-↑(x, y).1, (x, y).2).1.re

Tactic:
neg_re,

Goal state after:
case inr.inr.hf
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p ↦ (-↑p.1, p.2)) (x, y)
⊢ 0 < -(↑(x, y).1).re
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr
x y z : ℝ
x0 : 0 < x
x1 : x ≤ 1
zy : z ≤ y
⊢ x ^ y ≤ x ^ z

Tactic:
· exact Real.rpow_le_rpow_of_exponent_ge x0 x1 zy

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

Goal state before:
pp: case inl
x : ℝ
h : 0 ≤ x
⊢ x = x ^ (1 / 2) * x ^ (1 / 2)

Tactic:
← sq,

Goal state after:
case inl
x : ℝ
h : 0 ≤ x
⊢ x = (x ^ (1 / 2)) ^ 2
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_1.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
r₁ r₂ : R
hr₁ : 0 < r₁
left✝ : 0 < r₂
h : r₁ • x = r₂ • -y
⊢ ∃ g, ∑ i, g i • ![x, y] i = 0 ∧ ∃ i, g i ≠ 0

Tactic:
refine ⟨![r₁, r₂], ?_⟩

Goal state after:
case neg.refine_1.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
r₁ r₂ : R
hr₁ : 0 < r₁
left✝ : 0 < r₂
h : r₁ • x = r₂ • -y
⊢ ∑ i, ![r₁, r₂] i • ![x, y] i = 0 ∧ ∃ i, ![r₁, r₂] i ≠ 0
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
h : SameRay 𝕜 (x - y) (z - x)
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x - y = a • (z - y)
hzx : z - x = b • (z - y)
⊢ x ∈ [y -[𝕜] z]

Tactic:
rw [← mem_segment_translate _ (-x), neg_add_cancel]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
h : SameRay 𝕜 (x - y) (z - x)
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x - y = a • (z - y)
hzx : z - x = b • (z - y)
⊢ 0 ∈ [-x + y -[𝕜] -x + z]
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: case mp
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : AffineSubspace k V
hs : 0 ∈ s
x : V
⊢ x ∈ ↑s -ᵥ ↑s → x ∈ ↑s

pp: case mpr
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : AffineSubspace k V
hs : 0 ∈ s
x : V
⊢ x ∈ ↑s → x ∈ ↑s -ᵥ ↑s

Tactic:
· rintro ⟨a, ha, b, hb, rfl⟩
    simpa using s.smul_vsub_vadd_mem 1 ha hb hs

Goal state after:
case mpr
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : AffineSubspace k V
hs : 0 ∈ s
x : V
⊢ x ∈ ↑s → x ∈ ↑s -ᵥ ↑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
S : AffineSpace V P
t : Set (AffineSubspace k P)
p : P
h : ∀ s ∈ t, p ∈ s
v : V
hv : v ∈ ⨅ s ∈ t, s.direction
⊢ ∀ s ∈ t, v +ᵥ p ∈ s

Tactic:
intro s hs

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
t : Set (AffineSubspace k P)
p : P
h : ∀ s ∈ t, p ∈ s
v : V
hv : v ∈ ⨅ s ∈ t, s.direction
s : AffineSubspace k P
hs : s ∈ t
⊢ v +ᵥ p ∈ s
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
⊢ Absorbs 𝕜 s t ↔ ∀ᶠ (c : 𝕜) in 𝓝[≠] 0, MapsTo (fun x ↦ c • x) t s

Tactic:
rw [absorbs_iff_eventually_cobounded_mapsTo, ← Filter.inv_cobounded₀]; rfl

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

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ (fun x ↦ a • x) y ∈ r • s

Tactic:
have h'' : 1 ≤ ‖a⁻¹ • r‖ := by
    rw [norm_smul, norm_inv]
    exact one_le_mul_of_one_le_of_one_le ((one_le_inv₀ (norm_pos_iff.mpr h)).2 ha) hr

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
r : 𝕜
hr : 1 ≤ ‖r‖
h'' : 1 ≤ ‖a⁻¹ • r‖
⊢ (fun x ↦ a • x) y ∈ r • 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
p : P
ps : Set P
h : p ∈ ↑(affineSpan k ps)
⊢ affineSpan k (insert p ps) = affineSpan k ps

Tactic:
rw [← affineSpan_insert_affineSpan, Set.insert_eq_of_mem h, affineSpan_coe]

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✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
⊢ IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs; · simp
  rcases t.eq_empty_or_nonempty with rfl | ht; · simp
  simp [hs.ne_empty, ht.ne_empty, isVonNBounded_add_of_nonempty hs ht]

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
⊢ U ∈ 𝓝 0 → Absorbs 𝕜 U s

Tactic:
hU

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
⊢ Absorbs 𝕜 U s
Module: Mathlib.Topology.MetricSpace.Equicontinuity

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε
U : Set (α × α)
⊢ U ∈ 𝓤 α → ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
hU

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
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 b : P
⊢ ∑ i ∈ s, w i • (p -ᵥ b) = (∑ i ∈ s, w i) • (p -ᵥ b)

Tactic:
sum_smul

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 b : P
⊢ ∑ i ∈ s, w i • (p -ᵥ b) = ∑ i ∈ s, w i • (p -ᵥ b)
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
p₁ p₂ : P
v : V
⊢ v ∈ vectorSpan k {p₁, p₂} ↔ ∃ r, r • (p₁ -ᵥ p₂) = v

Tactic:
vectorSpan_pair,

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
p₁ p₂ : P
v : V
⊢ v ∈ k ∙ (p₁ -ᵥ p₂) ↔ ∃ r, r • (p₁ -ᵥ p₂) = v
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₁ w₂ : ι → k
p : ι → P
⊢ (s.weightedVSub p) w₁ +ᵥ (affineCombination k s p) w₂ = (affineCombination k s p) (w₁ + w₂)

Tactic:
rw [← vadd_eq_add, AffineMap.map_vadd, affineCombination_linear]

Goal state after:
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
pred : ι → Prop
inst✝ : DecidablePred pred
h : ∀ i ∈ s, w i ≠ 0 → pred i
⊢ (affineCombination k ({x ∈ s | pred x}) p) w = (affineCombination k s p) w

Tactic:
rw [affineCombination_apply, affineCombination_apply,
    s.weightedVSubOfPoint_filter_of_ne _ _ _ h]

Goal state after: