mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
⊢ ‖↑x‖ = |x|

Tactic:
rcases eq_or_ne x (p / (2 : ℝ)) with (rfl | hx')

Goal state after:
case inl
p✝ : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |p / 2| ≤ p / 2
⊢ ‖↑(p / 2)‖ = |p / 2|

case inr
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
⊢ ‖↑x‖ = |x|
Module: Mathlib.Analysis.SpecificLimits.Normed

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

Tactic:
by
  have ha : Antitone (fun n ↦ ∑ i ∈ range (2 * n + 1), (-1) ^ i * f i) := by
    refine antitone_nat_of_succ_le (fun n ↦ ?_)
    rw [show 2 * (n + 1) = 2 * n + 1 + 1 by ring, sum_range_succ, sum_range_succ]
    simp_rw [_root_.pow_succ', show (-1 : E) ^ (2 * n) = 1 by simp, neg_one_mul, neg_neg, one_mul,
      ← sub_eq_add_neg, sub_add_eq_add_sub, sub_le_iff_le_add]
    gcongr
    exact hfa (by lia)
  exact ha.le_of_tendsto (hfl.comp (tendsto_atTop_mono (fun n ↦ by dsimp; lia) tendsto_id)) _

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

Goal state before:
pp: case inr.inr.refine_1
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ -sin (arcsin x) = -x

Tactic:
sin_arcsin hx₁ hx₂

Goal state after:
case inr.inr.refine_1
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ -x = -x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ π / 4 ∈ Ioc (-(π / 2)) (π / 2)

Tactic:
have := pi_pos

Goal state after:
x : ℝ
this : 0 < π
⊢ π / 4 ∈ Ioc (-(π / 2)) (π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
this : cos (arcsin x) = √(1 - sin (arcsin x) ^ 2)
⊢ √(1 - sin (arcsin x) ^ 2) = √(1 - x ^ 2)

Tactic:
sin_arcsin hx₁ hx₂

Goal state after:
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
this : cos (arcsin x) = √(1 - sin (arcsin x) ^ 2)
⊢ √(1 - x ^ 2) = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arcsin x) / √(1 - x ^ 2) = x / √(1 - x ^ 2)

Tactic:
sin_arcsin hx₁ hx₂

Goal state after:
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ x / √(1 - x ^ 2) = x / √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arcsin x) = x

Tactic:
sin_arcsin hx₁ hx₂

Goal state after:
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ x = x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
by
  by_cases hx₁ : -1 ≤ x; swap
  · rw [not_le] at hx₁
    rw [arccos_of_le_neg_one hx₁.le, sin_pi, sqrt_eq_zero_of_nonpos]
    nlinarith
  by_cases hx₂ : x ≤ 1; swap
  · rw [not_le] at hx₂
    rw [arccos_of_one_le hx₂.le, sin_zero, sqrt_eq_zero_of_nonpos]
    nlinarith
  rw [arccos_eq_pi_div_two_sub_arcsin, sin_pi_div_two_sub, cos_arcsin]

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

Goal state before:
pp: z : ℂ
⊢ toIocMod Real.two_pi_pos (-π) z.im ∈ Ioc (-π) π

Tactic:
convert! toIocMod_mem_Ioc ..

Goal state after:
case e'_4.e'_4
z : ℂ
⊢ π = -π + 2 * π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
hx : x ≠ 0
⊢ cexp ↑(Real.log ‖x‖) * (↑(x.re / ‖x‖) + ↑(x.im / ‖x‖) * I) = x

Tactic:
← ofReal_exp,

Goal state after:
x : ℂ
hx : x ≠ 0
⊢ ↑(rexp (Real.log ‖x‖)) * (↑(x.re / ‖x‖) + ↑(x.im / ‖x‖) * I) = x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
⊢ ↑x.re + ↑(cexp ↑x.re * (cos ↑x.im + sin ↑x.im * I)).arg * I = x

Tactic:
← ofReal_exp,

Goal state after:
x : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
⊢ ↑x.re + ↑(↑(rexp x.re) * (cos ↑x.im + sin ↑x.im * I)).arg * I = x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case mpr.inl
⊢ log 0 = 0

Tactic:
simp only [log_one, log_zero, log_neg_eq_log]

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

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

Tactic:
simp only [log_one, log_zero, log_neg_eq_log]

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

Goal state before:
pp: case mpr.inr.inr
⊢ log (-1) = 0

Tactic:
simp only [log_one, log_zero, log_neg_eq_log]

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

Goal state before:
pp: ⊢ map cexp (comap cexp (𝓝 0)) = 𝓝[≠] 0

Tactic:
map_comap,

Goal state after:
⊢ 𝓝 0 ⊓ 𝓟 (range cexp) = 𝓝[≠] 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: ⊢ map cexp (comap cexp (cobounded ℂ)) = cobounded ℂ

Tactic:
map_comap,

Goal state after:
⊢ cobounded ℂ ⊓ 𝓟 (range cexp) = cobounded ℂ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ (fun x ↦ rexp (log b * x) * cos (x * π)) =o[atTop] fun _x ↦ 1 * 1

Tactic:
refine IsLittleO.mul_isBigO ?exp ?cos

Goal state after:
case exp
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ (fun x ↦ rexp (log b * x)) =o[atTop] fun _x ↦ 1

case cos
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ (fun x ↦ cos (x * π)) =O[atTop] fun _x ↦ 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x a : ℝ
⊢ a = 0 ^ x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
rw [← zero_rpow_eq_iff, eq_comm]

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

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

Tactic:
by
  simp only [rpow_def_of_pos hx, mul_add, exp_add]

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

Goal state before:
pp: θ ψ : Angle
hθs : θ.sign = 1
hψs : ψ.sign = 1
hsa : (θ + ψ).sign ≠ 1
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
← toReal_mem_Ioo_iff_sign_pos

Goal state after:
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: a b : ℂ
ha : a ≠ 0
⊢ (fun x ↦ a ^ x) = fun x ↦ cexp (Complex.log a * x)

Tactic:
ext1 b

Goal state after:
a b✝ : ℂ
ha : a ≠ 0
b : ℂ
⊢ a ^ b = cexp (Complex.log a * b)
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:
ext; exact Real.rpow_sub_natCast' (mod_cast x.2) h

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

Goal state before:
pp: case inl
p : ℝ × ℝ
hp : p.1 < 0
⊢ ContinuousAt (fun x ↦ log x.1) p

Tactic:
exact (continuousAt_log hp.ne).comp continuous_fst.continuousAt

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

Goal state before:
pp: x y : ℝ
hp : 0 < (x, y).2
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) (x, y)

Tactic:
dsimp only at hp

Goal state after:
x y : ℝ
hp : 0 < y
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) (x, y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x y : ℝ≥0∞
z : ℝ
hz : 0 ≤ z
⊢ (x * y⁻¹) ^ z = x ^ z / y ^ z

Tactic:
mul_rpow_of_nonneg _ _ hz,

Goal state after:
x y : ℝ≥0∞
z : ℝ
hz : 0 ≤ z
⊢ x ^ z * y⁻¹ ^ z = x ^ z / y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case coe
z : ℝ
hz : z < 0
x✝ : ℝ≥0
hx : 1 ≤ ↑x✝
⊢ ↑x✝ ^ z ≤ 1

Tactic:
simp only [one_le_coe_iff] at hx
    simp [← coe_rpow_of_ne_zero (ne_of_gt (lt_of_lt_of_le zero_lt_one hx)),
      NNReal.rpow_le_one_of_one_le_of_nonpos hx (le_of_lt hz)]

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

Goal state before:
pp: a b : ℝ
na da : ℕ
ha : IsNNRat a na da
nr dr : ℕ
hnum : IsNat (↑na ^ b) nr
hden : IsNat (↑da ^ b) dr
⊢ IsNNRat (a ^ b) nr dr

Tactic:
suffices IsNNRat (nr / dr : ℝ) nr dr by
    simpa [ha.to_eq, Real.div_rpow, hnum.1, hden.1]
  apply IsNNRat.of_raw
  rw [← hden.1]
  apply (Real.rpow_pos_of_pos _ _).ne'
  exact lt_of_le_of_ne' da.cast_nonneg ha.den_nz

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ ((lineMap x y) ⅟2 -ᵥ x) +ᵥ (lineMap x y) ⅟2 = y

Tactic:
lineMap_apply,

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
⊢ ((⅟2 • (y -ᵥ x) +ᵥ x) -ᵥ x) +ᵥ ⅟2 • (y -ᵥ x) +ᵥ 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 : P1
v : V1
c : k
⊢ (lineMap p (v +ᵥ p)) c = c • v +ᵥ p

Tactic:
lineMap_apply,

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 : P1
v : V1
c : k
⊢ c • ((v +ᵥ p) -ᵥ p) +ᵥ p = c • v +ᵥ p
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
inst✝¹ : IsDomain k
inst✝ : IsTorsionFree k V1
p₀ p₁ : P1
c₁ c₂ : k
⊢ (lineMap p₀ p₁) c₁ = (lineMap p₀ p₁) c₂ ↔ p₀ = p₁ ∨ c₁ = c₂

Tactic:
lineMap_apply,

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
inst✝¹ : IsDomain k
inst✝ : IsTorsionFree k V1
p₀ p₁ : P1
c₁ c₂ : k
⊢ c₁ • (p₁ -ᵥ p₀) +ᵥ p₀ = (lineMap p₀ p₁) c₂ ↔ p₀ = p₁ ∨ c₁ = c₂
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
inst✝¹ : IsDomain k
inst✝ : IsTorsionFree k V1
p₀ p₁ : P1
c₁ c₂ : k
⊢ c₁ • (p₁ -ᵥ p₀) +ᵥ p₀ = (lineMap p₀ p₁) c₂ ↔ p₀ = p₁ ∨ c₁ = c₂

Tactic:
lineMap_apply,

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
inst✝¹ : IsDomain k
inst✝ : IsTorsionFree k V1
p₀ p₁ : P1
c₁ c₂ : k
⊢ c₁ • (p₁ -ᵥ p₀) +ᵥ p₀ = c₂ • (p₁ -ᵥ p₀) +ᵥ p₀ ↔ p₀ = p₁ ∨ c₁ = c₂
Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V₁
inst✝¹⁰ : AddCommGroup V₂
inst✝⁹ : AddCommGroup V₃
inst✝⁸ : AddCommGroup V₄
inst✝⁷ : Module k V₁
inst✝⁶ : Module k V₂
inst✝⁵ : Module k V₃
inst✝⁴ : Module k V₄
inst✝³ : AffineSpace V₁ P₁
inst✝² : AffineSpace V₂ P₂
inst✝¹ : AffineSpace V₃ P₃
inst✝ : AffineSpace V₄ P₄
e : P₁ ≃ᵃ[k] P₂
p : P₂
v : V₂
⊢ v +ᵥ p = e.linear (e.linear.symm v) +ᵥ e.toEquiv (e.symm p)

Tactic:
LinearEquiv.apply_symm_apply,

Goal state after:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V₁
inst✝¹⁰ : AddCommGroup V₂
inst✝⁹ : AddCommGroup V₃
inst✝⁸ : AddCommGroup V₄
inst✝⁷ : Module k V₁
inst✝⁶ : Module k V₂
inst✝⁵ : Module k V₃
inst✝⁴ : Module k V₄
inst✝³ : AffineSpace V₁ P₁
inst✝² : AffineSpace V₂ P₂
inst✝¹ : AffineSpace V₃ P₃
inst✝ : AffineSpace V₄ P₄
e : P₁ ≃ᵃ[k] P₂
p : P₂
v : V₂
⊢ v +ᵥ p = v +ᵥ e.toEquiv (e.symm p)
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : CommRing 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : IsOrderedRing 𝕜
inst✝² : IsDomain 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
⊢ LinearIndependent 𝕜 ![t • y - x, s • y - x]

Tactic:
suffices H : LinearIndependent 𝕜 ![(-1 : 𝕜) • x + t • y, (-1 : 𝕜) • x + s • y] by
    convert! H using 1; simp only [neg_smul, one_smul]; abel_nf

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : CommRing 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : IsOrderedRing 𝕜
inst✝² : IsDomain 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
⊢ LinearIndependent 𝕜 ![-1 • x + t • y, -1 • x + s • y]
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 : y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
⊢ x + t • (y - x) ∈ [x -[𝕜] y]

Tactic:
rw [segment_eq_image']

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 : y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
⊢ x + t • (y - x) ∈ (fun θ ↦ x + θ • (y - x)) '' Icc 0 1
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
hxy : x ≠ y
h : x < y
⊢ openSegment 𝕜 x y = Ioo (min x y) (max x y)

pp: case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
hxy : x ≠ y
h : y < x
⊢ openSegment 𝕜 x y = Ioo (min x y) (max x y)

Tactic:
· rw [openSegment_eq_Ioo h, max_eq_right h.le, min_eq_left h.le]

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
hxy : x ≠ y
h : y < x
⊢ openSegment 𝕜 x y = Ioo (min x y) (max x y)
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z x : E
hx : x ∈ (fun x ↦ z + x) ⁻¹' s
y : E
hy : y ∈ (fun x ↦ z + x) ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ (fun x ↦ z + x) ⁻¹' s

Tactic:
have h := hs hx hy ha hb hab

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z x : E
hx : x ∈ (fun x ↦ z + x) ⁻¹' s
y : E
hy : y ∈ (fun x ↦ z + x) ⁻¹' s
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 ∈ s
⊢ a • x + b • y ∈ (fun x ↦ z + x) ⁻¹' s
Module: Mathlib.Analysis.Convex.Hull

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
h : (convexHull 𝕜) s = ∅
⊢ s = ∅

Tactic:
← Set.subset_empty_iff,

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
h : (convexHull 𝕜) s = ∅
⊢ s ⊆ ∅
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
⊢ Balanced 𝕜 (balancedCoreAux 𝕜 s)

Tactic:
by
  rintro a ha x ⟨y, hy, rfl⟩
  obtain rfl | h := eq_or_ne a 0
  · simp_rw [zero_smul, h0]
  rw [mem_balancedCoreAux_iff] at hy ⊢
  intro r hr
  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
  have h' := hy (a⁻¹ • r) h''
  rwa [smul_assoc, mem_inv_smul_set_iff₀ h] 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
v : E
hv : v ∈ s
w : E
hw : w ∈ t
x : E
hx : x ∈ s
y : E
hy : y ∈ t
h : (fun x1 x2 ↦ x1 + x2) v w ≠ (fun x1 x2 ↦ x1 + x2) x y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • (fun x1 x2 ↦ x1 + x2) v w + b • (fun x1 x2 ↦ x1 + x2) x y ∈ interior (s + t)

Tactic:
rw [smul_add, smul_add, add_add_add_comm]

Goal state after:
𝕜 : 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
v : E
hv : v ∈ s
w : E
hw : w ∈ t
x : E
hx : x ∈ s
y : E
hy : y ∈ t
h : (fun x1 x2 ↦ x1 + x2) v w ≠ (fun x1 x2 ↦ x1 + x2) x y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • v + b • x + (a • w + b • y) ∈ interior (s + t)
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y + (a • g x + b • g y) = a • (f x + g x) + b • (f y + g y)

Tactic:
rw [smul_add, smul_add, add_add_add_comm]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • f x + b • f y + (a • g x + b • g y) = a • (f x + g x) + b • (f y + g y)

Tactic:
rw [smul_add, smul_add, add_add_add_comm]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hg : StrictConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • f x + b • f y + (a • g x + b • g y) = a • (f x + g x) + b • (f y + g y)

Tactic:
rw [smul_add, smul_add, add_add_add_comm]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
⊢ ConvexOn 𝕜 s (f ⊔ g)

Tactic:
refine ⟨hf.left, fun x hx y hy a b ha hb hab => sup_le ?_ ?_⟩

Goal state after:
case refine_1
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ a • (f ⊔ g) x + b • (f ⊔ g) y

case refine_2
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ g (a • x + b • y) ≤ a • (f ⊔ g) x + b • (f ⊔ g) y
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:
simp [weightedVSubOfPoint, LinearMap.sum_apply]

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

Goal state before:
pp: case h
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₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ ↑s₁
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ ↑s₂
⊢ p₃ -ᵥ p₁ ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁) ∧ 0 + (p₃ -ᵥ p₁) = (fun x ↦ x -ᵥ p₁) p₃

Tactic:
and_comm,

Goal state after:
case h
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₁ s₂ : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ ↑s₁
hp₂ : p₂ ∈ s₂
p₃ : P
hp₃ : p₃ ∈ ↑s₂
⊢ 0 + (p₃ -ᵥ p₁) = (fun x ↦ x -ᵥ p₁) p₃ ∧ p₃ -ᵥ p₁ ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : Set P₁
⊢ map f (affineSpan k s) = affineSpan k (⇑f '' s)

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | ⟨p, hp⟩)

Goal state after:
case inl
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
⊢ map f (affineSpan k ∅) = affineSpan k (⇑f '' ∅)

case inr
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : Set P₁
p : P₁
hp : p ∈ s
⊢ map f (affineSpan k s) = affineSpan k (⇑f '' s)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (DFunLike.coe '' s)
⊢ (⨆ p, ⇑↑p) 0 = 0

Tactic:
rw [iSup_apply, ← @Real.iSup_const_zero s]
          congr!
          rename_i _ _ _ i
          exact map_zero i.1

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

Goal state before:
pp: case e'_2.e'_6
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 ι
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
p₁ p₂ : P
s' : Finset ι
h : ∑ i ∈ s, w i = 1
hp₂ : ∀ i ∈ s ∩ s', p i = p₂
hp₁ : ∀ i ∈ s \ s', p i = p₁
⊢ ∑ x ∈ s \ s', w x • (p x -ᵥ p₁) = 0

Tactic:
convert! Finset.sum_const_zero with i hi

Goal state after:
case e'_2.a
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 ι
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
p₁ p₂ : P
s' : Finset ι
h : ∑ i ∈ s, w i = 1
hp₂ : ∀ i ∈ s ∩ s', p i = p₂
hp₁ : ∀ i ∈ s \ s', p i = p₁
i : ι
hi : i ∈ s \ s'
⊢ w i • (p i -ᵥ p₁) = 0
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x₁ x₂ y : E
r : ℝ
⊢ x₁ - x₂ ∈ p.ball y r ↔ x₁ ∈ p.ball (x₂ + y) r

Tactic:
simp_rw [mem_ball, sub_sub]

Goal state after: