mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case refine_2
z : ℂ
⊢ (∃ θ, cexp (↑θ * I) = z) → ‖z‖ = 1

Tactic:
rintro ⟨θ, rfl⟩

Goal state after:
case refine_2
θ : ℝ
⊢ ‖cexp (↑θ * I)‖ = 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
h : 0 ≤ x
⊢ arcsin x = arccos √(1 - x ^ 2)

Tactic:
eq_comm,

Goal state after:
x : ℝ
h : 0 ≤ x
⊢ arccos √(1 - x ^ 2) = arcsin x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ z.arg ∈ Ioc (-π) π

Tactic:
have hπ : 0 < π := Real.pi_pos

Goal state after:
z : ℂ
hπ : 0 < π
⊢ z.arg ∈ Ioc (-π) π
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ |x * y| = |x| * |y|

Tactic:
abs_mul

Goal state after:
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ |x| * |y| = |x| * |y|
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg
x : ℂ
h : ¬x = 0
⊢ x.im / ‖x‖ / Real.cos x.arg = x.im / x.re

Tactic:
cos_arg h,

Goal state after:
case neg
x : ℂ
h : ¬x = 0
⊢ x.im / ‖x‖ / (x.re / ‖x‖) = x.im / x.re
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ 0 ≤ z.re ∧ z.im = 0 ↔ 0 ≤ z

Tactic:
eq_comm,

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

Goal state before:
pp: x : ℂ
hx_re : x.re < 0
hx_im : 0 ≤ x.im
⊢ x.arg = Real.arcsin ((-x).im / ‖x‖) + π

Tactic:
by
  simp only [arg, hx_re.not_ge, hx_im, if_true, if_false]

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

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

Tactic:
map_ne_zero

Goal state after:
case neg.hx
x : ℂ
hx : ¬x = 0
⊢ x ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ x ∈ s, f x ≠ 0
⊢ log (∏ i ∈ s, f i) = ∑ i ∈ s, log (f i)

Tactic:
by
  rw [← prod_map_toList, log_list_prod (by simp_all)]
  simp

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

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

Tactic:
eq_comm,

Goal state after:
θ : Angle
⊢ θ = -θ ↔ θ = 0 ∨ θ = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x y : ℂ
h : cexp x = cexp y
⊢ x.re = y.re

Tactic:
by
  obtain ⟨n, hn⟩ := exp_eq_exp_iff_exists_int.1 h
  simp [hn]

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

Goal state before:
pp: z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto log (𝓝[{z | z.im < 0}] z) (𝓝 (↑(Real.log ‖z‖) - ↑π * I))

Tactic:
convert!
    (continuous_ofReal.continuousAt.comp_continuousWithinAt
          (continuous_norm.continuousWithinAt.log _)).tendsto.add
      (((continuous_ofReal.tendsto _).comp <|
            tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero hre him).mul
        tendsto_const_nhds) using 1

Goal state after:
case e'_5
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ 𝓝 (↑(Real.log ‖z‖) - ↑π * I) = 𝓝 ((ofReal ∘ fun x ↦ Real.log ‖x‖) z + ↑(-π) * I)

case convert_1
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ‖z‖ ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case mpr.inr
⊢ 0 ^ 0 = 1

Tactic:
· exact cpow_zero _

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

Goal state before:
pp: case mp
x : ℂ
⊢ (∃ θ, cexp (↑θ * I) = x) → ∃ θ ∈ Ioc (-π) π, cexp (↑θ * I) = x

Tactic:
rintro ⟨θ, rfl⟩

Goal state after:
case mp
θ : ℝ
⊢ ∃ θ_1 ∈ Ioc (-π) π, cexp (↑θ_1 * I) = cexp (↑θ * I)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re < 0
⊢ ↑(↑(-x.re)).arg = ↑π + ↑π

Tactic:
arg_ofReal_of_nonneg (Left.neg_pos_iff.2 hr).le,

Goal state after:
case inr.inl.inl
x : ℂ
hx : x ≠ 0
hi : x.im = 0
hr : x.re < 0
⊢ ↑0 = ↑π + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
by
  induction θ using Real.Angle.induction_on with | _ θ
  simp [arg_mul_cos_add_sin_mul_I_eq_toIocMod hr]

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

Tactic:
convert!
    arg_mul_cos_add_sin_mul_I_coe_angle (mul_pos (norm_pos_iff.mpr hx) (norm_pos_iff.mpr hy))
      (arg x + arg y : Real.Angle) using 3
  simp_rw [← Real.Angle.coe_add, Real.Angle.sin_coe, Real.Angle.cos_coe, ofReal_cos, ofReal_sin,
    cos_add_sin_I, ofReal_add, add_mul, exp_add, ofReal_mul]
  rw [mul_assoc, mul_comm (exp _), ← mul_assoc (‖y‖ : ℂ), norm_mul_exp_arg_mul_I, mul_comm y, ←
    mul_assoc, norm_mul_exp_arg_mul_I]

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

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

Tactic:
arg_mul_coe_angle hx₀ hy₀,

Goal state after:
x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ (↑x.arg + ↑y.arg).toReal = x.arg + y.arg ↔ x.arg + y.arg ∈ Ioc (-π) π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
hre : z.re < 0
him✝ : z.im = 0
H : Tendsto (fun x ↦ Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : a✝.im < 0
⊢ a✝.re < 0 → Real.arcsin ((-a✝).im / ‖a✝‖) - π = a✝.arg

Tactic:
hre

Goal state after:
z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
H : Tendsto (fun x ↦ Real.arcsin ((-x).im / ‖x‖) - π) (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : a✝.im < 0
hre : a✝.re < 0
⊢ Real.arcsin ((-a✝).im / ‖a✝‖) - π = a✝.arg
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
hre : z.re < 0
him✝ : z.im = 0
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : 0 ≤ a✝.im
⊢ a✝.re < 0 → a✝.arg = Real.arcsin ((-a✝).im / ‖a✝‖) + π

Tactic:
hre

Goal state after:
z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : 0 ≤ a✝.im
hre : a✝.re < 0
⊢ a✝.arg = Real.arcsin ((-a✝).im / ‖a✝‖) + π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
n : ℤ
⊢ x ^ ↑n = x ^ n

Tactic:
simp only [rpow_def, ← Complex.ofReal_zpow, Complex.cpow_intCast, Complex.ofReal_intCast,
    Complex.ofReal_re]

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

Goal state before:
pp: case calc.step
x : ℝ
⊢ |x| ^ (log x)⁻¹ ≤ rexp 1

Tactic:
rw [← log_abs]

Goal state after:
case calc.step
x : ℝ
⊢ |x| ^ (log |x|)⁻¹ ≤ rexp 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) |(g a).im| b
x : α
hx : (fun x1 x2 ↦ x1 ≤ x2) |(g x).im| b
⊢ (fun x1 x2 ↦ x1 ≤ x2) |(f x).arg * (g x).im| (π * b)

Tactic:
abs_mul

Goal state after:
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) |(g a).im| b
x : α
hx : (fun x1 x2 ↦ x1 ≤ x2) |(g x).im| b
⊢ (fun x1 x2 ↦ x1 ≤ x2) (|(f x).arg| * |(g x).im|) (π * b)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
h : y + 1 ≠ 0
⊢ x ^ (y + 1) = x ^ y * x

Tactic:
rw [rpow_add' hx h, rpow_one]

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

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
h : 1 + y ≠ 0
⊢ x ^ (1 + y) = x * x ^ y

Tactic:
rw [rpow_add' hx h, rpow_one]

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

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

Tactic:
apply exp_injective

Goal state after:
x : ℝ
hx : 0 < x
y : ℝ
⊢ rexp (log (x ^ y)) = rexp (y * log x)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: p : ℝ × ℝ
hp_fst : p.1 < 0
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.1 < 0
x : ℝ × ℝ
hx : x.1 < 0
⊢ x.1 ^ x.2 = rexp (log x.1 * x.2) * cos (x.2 * π)

Tactic:
rpow_def_of_neg hx

Goal state after:
p : ℝ × ℝ
hp_fst : p.1 < 0
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.1 < 0
x : ℝ × ℝ
hx : x.1 < 0
⊢ rexp (log x.1 * x.2) * cos (x.2 * π) = rexp (log x.1 * x.2) * cos (x.2 * π)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x y : ℝ≥0
z : ℝ
hz : 0 < z
⊢ x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y

Tactic:
rw [← rpow_le_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz.ne']

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

Goal state before:
pp: x y : ℝ≥0
z : ℝ
hz : 0 < z
⊢ x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z

Tactic:
rw [← rpow_le_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz.ne']

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

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ x ^ (-z) ≤ y ^ (-z)

Tactic:
refine rpow_le_rpow ?_ hxy (neg_nonneg.2 hz)

Goal state after:
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case inr
x : ℝ
⊢ ContinuousAt (fun x ↦ x ^ 0) x

Tactic:
simp_rw [rpow_zero]; exact continuousAt_const

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

Goal state before:
pp: case inr
x ε : ℝ
hx : 0 ≤ x
hε : 0 < ε
h : 0 < x
⊢ ε * log x ≤ x ^ ε

Tactic:
exact (log_rpow h ε).symm.trans_le <| (log_le_sub_one_of_pos <| rpow_pos_of_pos h ε).trans
    (sub_one_lt _).le

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

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

Tactic:
lift x to ℝ≥0 using ne_of_lt (lt_of_lt_of_le hx2 le_top)
  simp only [coe_lt_one_iff, coe_pos] at hx1 hx2 ⊢
  simp [← coe_rpow_of_ne_zero (ne_of_gt hx1), NNReal.one_lt_rpow_of_pos_of_lt_one_of_neg hx1 hx2 hz]

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

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

Tactic:
simp [H]

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

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

Tactic:
rw [← Ne] at hp0

Goal state after:
case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : p ≠ 0
hx0 : x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton M
x y : M
⊢ SameRay R x y

Tactic:
rw [Subsingleton.elim x 0]

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton M
x y : M
⊢ SameRay R 0 y
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
p₁ p₂ p : P
⊢ p -ᵥ midpoint R p₁ p₂ = ⅟2 • (p -ᵥ p₁) + ⅟2 • (p -ᵥ p₂)

Tactic:
← neg_vsub_eq_vsub_rev,

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
p₁ p₂ p : P
⊢ -(midpoint R p₁ p₂ -ᵥ p) = ⅟2 • (p -ᵥ p₁) + ⅟2 • (p -ᵥ 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 y : P
⊢ x = midpoint R x y ↔ x = y

Tactic:
eq_comm,

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
⊢ midpoint R x y = x ↔ x = y
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
⊢ y = midpoint R x y ↔ x = y

Tactic:
eq_comm,

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
⊢ midpoint R x y = y ↔ x = y
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p₀ p₁ : P1
c : k
⊢ p₀ -ᵥ (lineMap p₀ p₁) c = c • (p₀ -ᵥ p₁)

Tactic:
← neg_vsub_eq_vsub_rev,

Goal state after:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p₀ p₁ : P1
c : k
⊢ -((lineMap p₀ p₁) c -ᵥ p₀) = c • (p₀ -ᵥ p₁)
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s : Set E
⊢ (∀ ⦃y : E⦄, y ∈ s → [x -[𝕜] y] ⊆ s) → StarConvex 𝕜 x s

Tactic:
rintro h y hy a b ha hb hab

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s : Set E
h : ∀ ⦃y : E⦄, y ∈ s → [x -[𝕜] y] ⊆ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : 0 + b = 1
⊢ 0 • x + b • y ∈ s

pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
⊢ a • x + b • y ∈ s

Tactic:
· rw [zero_add] at hab
    rwa [hab, zero_smul, one_smul, zero_add]

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
⊢ a • x + b • y ∈ s
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : Ring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : IsStrictOrderedModule 𝕜 E
inst✝ : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
⊢ b • z ≤ (a + b) • x - a • y

Tactic:
rwa [le_sub_iff_add_le', hab, one_smul]

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

Goal state before:
pp: case p
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
x✝ : P
| x✝ ∈ ↑s ∧ x✝ -ᵥ p = -v

Tactic:
← neg_vsub_eq_vsub_rev,

Goal state after:
case p
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
x✝ : P
| x✝ ∈ ↑s ∧ -(p -ᵥ x✝) = -v
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : CommSemiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b : E
⊢ Convex 𝕜 (openSegment 𝕜 a b)

Tactic:
convex_iff_openSegment_subset

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : CommSemiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b : E
⊢ ∀ ⦃x : E⦄, x ∈ openSegment 𝕜 a b → ∀ ⦃y : E⦄, y ∈ openSegment 𝕜 a b → openSegment 𝕜 x y ⊆ openSegment 𝕜 a b
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: case inl.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hxy : x ≤ y
⊢ x ≤ a • x + b • y

Tactic:
calc
        x = a • x + b • x := (Convex.combo_self hab _).symm
        _ ≤ a • x + b • y := by gcongr

Goal state after:
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
⊢ ⨅ s ∈ t, s.direction ≤ (sInf t).direction

Tactic:
intro v hv

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
⊢ v ∈ (sInf t).direction
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z x : E
hx : x ∈ (fun x ↦ z + x) ⁻¹' s
y : E
hy : y ∈ (fun x ↦ z + x) ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h : a • (fun x ↦ z + x) x + b • (fun x ↦ z + x) y ∈ interior s
⊢ a • x + b • y ∈ (fun x ↦ z + x) ⁻¹' interior s

Tactic:
rwa [smul_add, smul_add, add_add_add_comm, ← _root_.add_smul, hab, one_smul] at h

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✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
⊢ StrictConvex 𝕜 (s + t)

Tactic:
by
  rintro _ ⟨v, hv, w, hw, rfl⟩ _ ⟨x, hx, y, hy, rfl⟩ h a b ha hb hab
  rw [smul_add, smul_add, add_add_add_comm]
  obtain rfl | hvx := eq_or_ne v x
  · refine interior_mono (add_subset_add (singleton_subset_iff.2 hv) Subset.rfl) ?_
    rw [Convex.combo_self hab, singleton_add]
    exact
      (isOpenMap_add_left _).image_interior_subset _
        (mem_image_of_mem _ <| ht hw hy (ne_of_apply_ne _ h) ha hb hab)
  exact
    subset_interior_add_left
      (add_mem_add (hs hv hx hvx ha hb hab) <| ht.convex hw hy ha.le hb.le hab)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
x y : E
inst✝ : AddRightStrictMono 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ x + t • y ∈ interior s

Tactic:
by
  have h : x + t • y = (1 - t) • x + t • (x + y) := by match_scalars <;> simp
  rw [h]
  exact hs hx hxy (fun h => hy <| add_left_cancel (a := x) (by rw [← h, add_zero]))
    (sub_pos_of_lt ht₁) ht₀ (sub_add_cancel 1 t)

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✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
c : P
hc : c ∈ s
r : k
p : P
hp : p ∈ s
⊢ (homothety c r) p ∈ s

Tactic:
rw [AffineMap.homothety_eq_lineMap]
  exact lineMap_mem r hc hp

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
s : Set P
h₁ : s.Subsingleton
p : P
h₂ : {p} = univ
hp : p ∈ s
this : s = {p}
⊢ Subsingleton P

Tactic:
eq_comm,

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
s : Set P
h₁ : s.Subsingleton
p : P
h₂ : univ = {p}
hp : p ∈ s
this : s = {p}
⊢ Subsingleton P
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
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
this : s = {p}
⊢ {p} = univ

Tactic:
eq_comm,

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
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
this : s = {p}
⊢ univ = {p}
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
b : P
⊢ (s.weightedVSubOfPoint p b) w = ∑ i ∈ s, w i • (p i -ᵥ b)

Tactic:
by
  simp [weightedVSubOfPoint, LinearMap.sum_apply]

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
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
p₂ p : P
⊢ (∃ y ∈ k ∙ (p₂ -ᵥ p₁), ∃ z ∈ s.direction, y + z = p -ᵥ p₁) → ∃ r, ∃ p0 ∈ s, p = r • (p₂ -ᵥ p₁) +ᵥ p0

Tactic:
rintro ⟨v₁, hv₁, v₂, hv₂, hp⟩
    rw [Submodule.mem_span_singleton] at hv₁
    rcases hv₁ with ⟨r, rfl⟩
    use r, v₂ +ᵥ p₁, vadd_mem_of_mem_direction hv₂ hp₁
    symm at hp
    rw [← sub_eq_zero, ← vsub_vadd_eq_vsub_sub, vsub_eq_zero_iff_eq] at hp
    rw [hp, vadd_vadd]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ
ha : 0 ≤ a
h : ∀ i ∈ s, (p i) x ≤ a
⊢ (s.sup p) x ≤ a

Tactic:
by
  lift a to ℝ≥0 using ha
  rw [finset_sup_apply, NNReal.coe_le_coe]
  exact Finset.sup_le h

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
h : ⊥ = map (↑(constVAdd k P v)) s
⊢ s = ⊥

Tactic:
eq_comm,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
h : map (↑(constVAdd k P v)) s = ⊥
⊢ s = ⊥
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 1
p : ι → P
hnz : ∑ i ∈ s, w i ≠ 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (Function.const ι 0) i1 1
hw1 : ∑ i ∈ s, w1 i = 1
hw1s : (Finset.affineCombination k s p) w1 = p i1
hv : (Finset.affineCombination k s p) w -ᵥ p i1 ∈ (affineSpan k (Set.range p)).direction
⊢ (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)

Tactic:
rw [← vsub_vadd (s.affineCombination k p w) (p i1)]

Goal state after:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 1
p : ι → P
hnz : ∑ i ∈ s, w i ≠ 0
i1 : ι
hi1 : i1 ∈ s
w1 : ι → k := Function.update (Function.const ι 0) i1 1
hw1 : ∑ i ∈ s, w1 i = 1
hw1s : (Finset.affineCombination k s p) w1 = p i1
hv : (Finset.affineCombination k s p) w -ᵥ p i1 ∈ (affineSpan k (Set.range p)).direction
⊢ ((Finset.affineCombination k s p) w -ᵥ p i1) +ᵥ p i1 ∈ affineSpan k (Set.range p)