mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find h
⊢ ∃ i, ∀ j ≥ i, |f j - f i| < ε

Tactic:
have hl : ∀ n : ℕ, n ≥ m → f n > a - l • ε := Nat.find_spec h

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find h
hl : ∀ n ≥ m, f n > a - l • ε
⊢ ∃ i, ∀ j ≥ i, |f j - f i| < ε
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: n : ℕ
hn : 0 < n
x : ℂ
hx : x ∈ {y | ‖y‖ < 1}
⊢ ↑n.succ / (↑n ! * ↑n) * ‖x ^ n‖ = ‖x‖ ^ n * (↑n.succ * (↑n ! * ↑n)⁻¹)

Tactic:
simp [field]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: a ε : ℝ
this✝ : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
x : ℂ
a✝ : x.re ≤ a
y : ℂ
hy : y.re ≤ a
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
this : cexp x - cexp y = cexp y * (cexp (x - y) - 1)
hε : 0 < ε
hδ : 0 < δ ∧ ∀ ⦃y : ℂ⦄, ‖y‖ < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
hya : Real.exp y.re ≤ Real.exp a
⊢ ε / (2 * Real.exp a) * Real.exp a < ε

Tactic:
simp [field]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: n : ℕ
x : ℝ
⊢ ((fun r ↦ r⁻¹) ∘ fun x ↦ rexp x / x ^ n) x = x ^ n * rexp (-x)

Tactic:
comp_apply,

Goal state after:
n : ℕ
x : ℝ
⊢ (rexp x / x ^ n)⁻¹ = x ^ n * rexp (-x)
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
x : M ⧸ S
r : ℝ
⊢ ‖x‖ < r ↔ ∃ m, ↑m = x ∧ ‖m‖ < r

Tactic:
by
  simp [norm_eq_infDist, infDist_lt_iff (norm_aux _)]

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

Goal state before:
pp: x : ℝ
hx₁ : -π < x
hx₂ : x < π
h : x ≠ 0
x✝ : x < 0 ∨ 0 < x
⊢ sin x ≠ 0

Tactic:
cases h.lt_or_gt with

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ {x} / sphere 1 δ = sphere x δ

Tactic:
by
  rw [singleton_div_sphere, div_one]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ frontier (closedBall x r) = sphere x r

Tactic:
rw [frontier, closure_closedBall, interior_closedBall' x r, closedBall_sdiff_ball]

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

Goal state before:
pp: K : Type u_4
inst✝ : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
⊢ HasSum (fun n ↦ ξ ^ n) (1 - ξ)⁻¹

Tactic:
have xi_ne_one : ξ ≠ 1 := by
    contrapose! h
    simp [h]

Goal state after:
K : Type u_4
inst✝ : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
⊢ HasSum (fun n ↦ ξ ^ n) (1 - ξ)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ Function.Periodic tan ↑π

Tactic:
simpa only [tan_eq_sin_div_cos] using! sin_antiperiodic.div cos_antiperiodic

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
g : C(X, Y)
⊢ g ∈ closure {x | MapsTo (⇑x) K V} → MapsTo (⇑(id g)) K U

Tactic:
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.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
a : X
b : Y
⊢ (a, b) ∈ pathComponent (x, y) ↔ (a, b) ∈ pathComponent x ×ˢ pathComponent y

Tactic:
simp only [Set.mem_prod, mem_pathComponent_iff]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
a : X
b : Y
⊢ Joined (x, y) (a, b) ↔ Joined x a ∧ Joined y b
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:
rw [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.Topology.Connected.PathConnected

Goal state before:
pp: ι : Type u_3
Z : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (Z i)
x : (i : ι) → Z i
⊢ pathComponent x = univ.pi fun i ↦ pathComponent (x i)

Tactic:
by
  ext y
  simp only [Set.mem_univ_pi, mem_pathComponent_iff]
  exact ⟨fun h i ↦ h.map (continuous_apply i), fun h ↦ .pi h⟩

Goal state after:
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
f : Y → Path x y
g : Y → Path y z
hf : Continuous[inst✝, _] f
⊢ Continuous[inst✝, _] g → Continuous[inst✝, _] fun t ↦ (f t).trans (g t)

Tactic:
hg

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
f : Y → Path x y
g : Y → Path y z
hf : Continuous[inst✝, _] f
hg : Continuous[inst✝, _] g
⊢ Continuous[inst✝, _] fun t ↦ (f t).trans (g t)
Module: Mathlib.Algebra.Order.Ring.Interval

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
r : R
hr : 0 < r
k m : ℤ
h : r * ↑k ∈ Set.Ioo (r * ↑(m - 1)) (r * ↑(m + 1))
⊢ k = m

Tactic:
by
  simpa using int_mem_Icc_of_mul_mem_Ioo hr h

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

Goal state before:
pp: p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
m : ℕ
hm : ↑(↑m / ↑(addOrderOf u) * p) = u
⊢ ‖↑(↑m / ↑(addOrderOf u) * p)‖ = p * (↑(min (m % n) (n - m % n)) / ↑n)

Tactic:
norm_div_natCast

Goal state after:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
m : ℕ
hm : ↑(↑m / ↑(addOrderOf u) * p) = u
⊢ p * (↑(min (m % addOrderOf u) (addOrderOf u - m % addOrderOf u)) / ↑(addOrderOf u)) =
    p * (↑(min (m % n) (n - m % n)) / ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : ¬(-(π / 2) ≤ θ ∧ θ ≤ π / 2)
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Tactic:
not_and_or,

Goal state after:
case neg
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : ¬-(π / 2) ≤ θ ∨ ¬θ ≤ π / 2
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case neg
x : ℝ
hx0 : ¬x < 0
⊢ 2 * x ≤ rexp x

Tactic:
· apply le_trans (mul_le_mul_of_nonneg_right _ (le_of_not_gt hx0)) exp_one_mul_le_exp
    have := Real.add_one_le_exp 1
    rwa [one_add_one_eq_two] at this

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

Goal state before:
pp: θ : Angle
⊢ 2 • θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑π

Tactic:
by
  rw [← not_or, ← 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 ∘ fun x ↦ log (x + y) - log x) x

Tactic:
comp_apply,

Goal state after:
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) - log x)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x y : ℂ
⊢ ¬(x = 0 ∧ y ≠ 0) ↔ x ≠ 0 ∨ y = 0

Tactic:
not_and_or,

Goal state after:
x y : ℂ
⊢ ¬x = 0 ∨ ¬y ≠ 0 ↔ x ≠ 0 ∨ y = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mpr
θ ψ : ℝ
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π → sin θ = sin ψ

Tactic:
rw [angle_eq_iff_two_pi_dvd_sub, ← eq_sub_iff_add_eq, ← coe_sub, angle_eq_iff_two_pi_dvd_sub]

Goal state after:
case mpr
θ ψ : ℝ
⊢ ((∃ k, θ - ψ = 2 * π * ↑k) ∨ ∃ k, θ - (π - ψ) = 2 * π * ↑k) → sin θ = sin ψ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I_coe_angle zero_lt_one]

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

Goal state before:
pp: y : ℝ
hy : 0 < y
b : ℝ
hb : 0 ≤ b
x : ℝ
hx₀ : 0 ≤ x
hx : b ^ (1 / y) ≤ x
⊢ x ^ y ∈ Set.Ici b

Tactic:
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: case mpr
x a : ℝ
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 → 0 ^ x = a

Tactic:
· rintro (⟨h, rfl⟩ | ⟨rfl, rfl⟩)
    · exact zero_rpow h
    · exact rpow_zero _

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

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

Tactic:
split_ifs <;>
    simp [Complex.ofReal_log hx]

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

Goal state before:
pp: case hgf
a : ℝ
ha : 0 < a
b t : ℝ
ht : 0 < t
h : t = 0 ∧ b ≠ 0
⊢ rexp (-a * t) = 0

Tactic:
exact (ht.ne' h.1).elim

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

Goal state before:
pp: a : ℝ
ha : 0 < a
b : ℝ
⊢ (fun x ↦ rexp (-a * x)) =o[atTop] fun x ↦ x ^ b

Tactic:
apply isLittleO_of_tendsto'
  · 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
  · refine (tendsto_exp_mul_div_rpow_atTop (-b) a ha).inv_tendsto_atTop.congr' ?_
    refine (eventually_ge_atTop 0).mono fun t ht => ?_
    simp [field, Real.exp_neg, rpow_neg ht]

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

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

Tactic:
← or_assoc

Goal state after:
x q : ℝ
h : (x ≠ 0 ∨ 0 < q) ∨ 0 = q
⊢ ContinuousAt (fun x ↦ x ^ q) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: z w : ℂ
h₁ : ¬((z, w).1 ≤ 0 ∧ (z, w).1 ≠ 0)
h₂ : 0 < (z, w).2.re
⊢ ContinuousAt (fun x ↦ x.1 ^ x.2) (z, w)

Tactic:
not_and_or,

Goal state after:
z w : ℂ
h₁ : ¬(z, w).1 ≤ 0 ∨ ¬(z, w).1 ≠ 0
h₂ : 0 < (z, w).2.re
⊢ ContinuousAt (fun x ↦ x.1 ^ x.2) (z, w)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ x ^ y < x ^ z

Tactic:
by
  repeat' rw [rpow_def_of_pos hx0]
  rw [exp_lt_exp]; exact mul_lt_mul_of_neg_left hyz (log_neg hx0 hx1)

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

Goal state before:
pp: case pos.inl
y : ℝ
x : ℝ≥0
h : x = 0
H : y < 0
⊢ ↑x ^ y = 0 ↔ ↑x = 0 ∧ 0 < y ∨ ↑x = ∞ ∧ y < 0

Tactic:
simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]

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

Goal state before:
pp: case pos.inr.inl
y : ℝ
x : ℝ≥0
h : x = 0
H : y = 0
⊢ ↑x ^ y = 0 ↔ ↑x = 0 ∧ 0 < y ∨ ↑x = ∞ ∧ y < 0

Tactic:
simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]

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

Goal state before:
pp: case pos.inr.inr
y : ℝ
x : ℝ≥0
h : x = 0
H : 0 < y
⊢ ↑x ^ y = 0 ↔ ↑x = 0 ∧ 0 < y ∨ ↑x = ∞ ∧ y < 0

Tactic:
simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]

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

Goal state before:
pp: case pos.inl
y : ℝ
x : ℝ≥0
h : x = 0
H : y < 0
⊢ ↑x ^ y = ∞ ↔ ↑x = 0 ∧ y < 0 ∨ ↑x = ∞ ∧ 0 < y

Tactic:
simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]

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

Goal state before:
pp: case pos.inr.inl
y : ℝ
x : ℝ≥0
h : x = 0
H : y = 0
⊢ ↑x ^ y = ∞ ↔ ↑x = 0 ∧ y < 0 ∨ ↑x = ∞ ∧ 0 < y

Tactic:
simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]

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

Goal state before:
pp: case pos.inr.inr
y : ℝ
x : ℝ≥0
h : x = 0
H : 0 < y
⊢ ↑x ^ y = ∞ ↔ ↑x = 0 ∧ y < 0 ∨ ↑x = ∞ ∧ 0 < y

Tactic:
simp [h, H, zero_rpow_of_neg, zero_rpow_of_pos, le_of_lt]

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

Goal state before:
pp: case neg
y z : ℝ
hyz : 0 < y + z
hx : 0 ≠ ∞
hy' : ¬0 < y
⊢ 0 ^ (y + z) = 0 ^ y * 0 ^ z

Tactic:
· have hz' : 0 < z := by linarith
      simp [ENNReal.zero_rpow_of_pos hyz, ENNReal.zero_rpow_of_pos hz']

Goal state after:
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

Goal state after:
case inr
x : ℝ
h : x < 0
this : 1 / 2 * π = π / 2
⊢ √x = x ^ (1 / 2)
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)

pp: case neg
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:
case neg
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
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 x' y y' : P
⊢ midpoint R x y = midpoint R x' y' ↔ x -ᵥ x' = y' -ᵥ y

Tactic:
rw [← @vsub_eq_zero_iff_eq V, midpoint_vsub_midpoint, midpoint_eq_iff, pointReflection_apply,
    vsub_eq_sub, zero_sub, vadd_eq_add, add_zero, neg_eq_iff_eq_neg, neg_vsub_eq_vsub_rev]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
v✝ : M
hv✝ : v✝ ≠ 0
⊢ -u • rayOfNeZero R v✝ hv✝ = -(u • rayOfNeZero R v✝ hv✝)

Tactic:
simp only [smul_rayOfNeZero, Units.smul_def, Units.val_neg, neg_smul, neg_rayOfNeZero]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a x b c : E
⊢ a +ᵥ x ∈ a +ᵥ [b -[𝕜] c] ↔ x ∈ [b -[𝕜] c]

Tactic:
vadd_mem_vadd_set_iff

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a x b c : E
⊢ a +ᵥ x ∈ a +ᵥ openSegment 𝕜 b c ↔ x ∈ openSegment 𝕜 b c

Tactic:
vadd_mem_vadd_set_iff

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : x + y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
⊢ x + t • y = (1 - t) • x + t • (x + y)

Tactic:
rw [smul_add, ← add_assoc, ← add_smul, sub_add_cancel, one_smul]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : x + y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
⊢ x + t • y ∈ s

Tactic:
have h : x + t • y = (1 - t) • x + t • (x + y) := by
    rw [smul_add, ← add_assoc, ← add_smul, sub_add_cancel, one_smul]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : x + y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ x + t • y ∈ s
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x ≤ y
⊢ Icc x y = Icc (min x y) (max x y)

Tactic:
max_eq_right h,

Goal state after:
case inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x ≤ y
⊢ Icc x y = Icc (min x y) y
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 : Set P
s₁ : AffineSubspace k P
h : s ⊆ ↑s₁
p p₁ : P
hp₁ : p₁ ∈ s
v : V
hv : v ∈ vectorSpan k s
hp : p = v +ᵥ p₁
hp₁s₁ : p₁ ∈ ↑s₁
⊢ v ∈ s₁.direction

Tactic:
have hs : vectorSpan k s ≤ s₁.direction := vectorSpan_mono k h

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 : Set P
s₁ : AffineSubspace k P
h : s ⊆ ↑s₁
p p₁ : P
hp₁ : p₁ ∈ s
v : V
hv : v ∈ vectorSpan k s
hp : p = v +ᵥ p₁
hp₁s₁ : p₁ ∈ ↑s₁
hs : vectorSpan k s ≤ s₁.direction
⊢ v ∈ s₁.direction
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 : Set (AffineSubspace k P)
c : k
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ ⋂ s' ∈ s, ↑s'
hp₂ : p₂ ∈ ⋂ s' ∈ s, ↑s'
hp₃ : p₃ ∈ ⋂ s' ∈ s, ↑s'
s₂ : AffineSubspace k P
hs₂ : s₂ ∈ s
⊢ c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ ↑s₂

Tactic:
Set.mem_iInter₂

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 : Set (AffineSubspace k P)
c : k
p₁ p₂ p₃ : P
hp₁ : ∀ i ∈ s, p₁ ∈ ↑i
hp₂ : ∀ i ∈ s, p₂ ∈ ↑i
hp₃ : ∀ i ∈ s, p₃ ∈ ↑i
s₂ : AffineSubspace k P
hs₂ : s₂ ∈ s
⊢ c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ ↑s₂
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁷ : NormedDivisionRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
s : Set E
inst✝⁴ : NormedRing 𝕝
inst✝³ : Module 𝕜 𝕝
inst✝² : NormSMulClass 𝕜 𝕝
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖b‖
⊢ a • s ⊆ b • s

Tactic:
by
  obtain rfl | hb := eq_or_ne b 0
  · rw [norm_zero, norm_le_zero_iff] at h
    simp only [h, ← image_smul, zero_smul, Subset.rfl]
  · calc
      a • s = b • (b⁻¹ • a) • s := by rw [smul_assoc, smul_inv_smul₀ hb]
      _ ⊆ b • s := smul_set_mono <| hs _ <| by
        rw [norm_smul, norm_inv, ← div_eq_inv_mul]
        exact div_le_one_of_le₀ h (norm_nonneg _)

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

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
A : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
a : 𝕜
ha : ‖a‖ ≤ 1
h : a ≠ 0
⊢ (fun x ↦ a • x) '' insert 0 (interior A) ⊆ insert 0 (interior A)

Tactic:
image_insert_eq,

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
A : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
a : 𝕜
ha : ‖a‖ ≤ 1
h : a ≠ 0
⊢ insert (a • 0) ((fun x ↦ a • x) '' interior A) ⊆ insert 0 (interior A)
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : PartialOrder 𝕜
hs : Balanced 𝕜 s
x : E
hx : x ∈ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull 𝕜) s}
y : E
hy : y ∈ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull 𝕜) s}
u v : 𝕜
hu : 0 ≤ u
hv : 0 ≤ v
huv : u + v = 1
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ u • a • x + v • a • y ∈ (convexHull 𝕜) s

Tactic:
exact convex_convexHull 𝕜 s (hx a ha) (hy a ha) hu hv huv

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
ι : Sort u_6
s : ι → Set E
hdir : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)
⊢ StrictConvex 𝕜 (⋃ i, s i)

Tactic:
rintro x hx y hy hxy a b ha hb hab
  rw [mem_iUnion] at hx hy
  obtain ⟨i, hx⟩ := hx
  obtain ⟨j, hy⟩ := hy
  obtain ⟨k, hik, hjk⟩ := hdir i j
  exact interior_mono (subset_iUnion s k) (hs (hik hx) (hjk hy) hxy ha hb hab)

Goal state after:
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
S : AffineSpace V P
p₁ p₂ : P
⊢ p₁ ∈ affineSpan k {p₂} ↔ p₁ = p₂

Tactic:
simp [← mem_coe]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case refine_1
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 : Set P
p : P
hp : p ∈ s
⊢ Submodule.span k (s -ᵥ s) ≤ Submodule.span k ((fun x ↦ p -ᵥ x) '' s)

Tactic:
rw [Submodule.span_le]
    rintro v ⟨p₁, hp₁, p₂, hp₂, hv⟩
    simp_rw [← vsub_sub_vsub_cancel_left p₁ p₂ p] at hv
    rw [← hv, SetLike.mem_coe, Submodule.mem_span]
    exact fun m hm => Submodule.sub_mem _ (hm ⟨p₂, hp₂, rfl⟩) (hm ⟨p₁, hp₁, rfl⟩)

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case mp
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₂ : P
⊢ p ∈ line[k, p₁, p₂] → ∃ r, (AffineMap.lineMap p₁ p₂) r = p

pp: case mpr
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₂ : P
⊢ (∃ r, (AffineMap.lineMap p₁ p₂) r = p) → p ∈ line[k, p₁, p₂]

Tactic:
· intro h
    rw [← vsub_vadd p p₁, vadd_left_mem_affineSpan_pair] at h
    obtain ⟨r, hr⟩ := h
    refine ⟨r, ?_⟩
    rw [← vsub_vadd p p₁, ← hr, AffineMap.lineMap_apply]

Goal state after:
case mpr
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₂ : P
⊢ (∃ r, (AffineMap.lineMap p₁ p₂) r = p) → p ∈ line[k, p₁, p₂]
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
⊢ StrictConvexOn 𝕜 s (-f) → StrictConcaveOn 𝕜 s f

Tactic:
rintro ⟨hconv, h⟩
    refine ⟨hconv, fun x hx y hy hxy a b ha hb hab => ?_⟩
    simp only [ne_eq, Pi.neg_apply, smul_neg, lt_add_neg_iff_add_lt, add_comm,
      add_neg_lt_iff_lt_add] at h
    exact h hx hy hxy ha hb hab

Goal state after: