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

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
⊢ Disjoint (ball x δ) (closedBall y ε) ↔ δ + ε ≤ dist x y

Tactic:
refine ⟨fun h => le_of_not_gt fun hxy => ?_, ball_disjoint_closedBall⟩
  rw [add_comm] at hxy
  obtain ⟨z, hxz, hzy⟩ := exists_dist_lt_le hδ hε hxy
  rw [dist_comm] at hxz
  exact h.le_bot ⟨hxz, hzy⟩

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

Goal state before:
pp: 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))
⊢ ∀ᶠ (x : ℕ) in atTop, ‖↑((x + k).choose k)‖ ≤ 2 ^ k * ‖↑(x ^ k)‖

Tactic:
filter_upwards [Ioi_mem_atTop k] with n (hn : k < n)

Goal state after:
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))
n : ℕ
hn : k < n
⊢ ‖↑((n + k).choose k)‖ ≤ 2 ^ k * ‖↑(n ^ k)‖
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n ↦ if n < N then 0 else u n
hC : 0 ≤ C
⊢ ∀ n ≥ N, u n = v n

Tactic:
intro n hn

Goal state after:
α : Type u_1
inst✝ : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n ↦ if n < N then 0 else u n
hC : 0 ≤ C
n : ℕ
hn : n ≥ N
⊢ u n = v n
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case mk
X : Type u_1
inst✝ : TopologicalSpace X
b✝ : ZerothHomotopy X
x : X
⊢ ∃ a, mk a = Quot.mk (⇑(pathSetoid X)) x

Tactic:
exact ⟨x, rfl⟩

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
motive : ZerothHomotopy X → Prop
mk : ∀ (x : X), motive (ZerothHomotopy.mk x)
x : ZerothHomotopy X
⊢ motive x

Tactic:
obtain ⟨x, rfl⟩ := mk_surjective x
  exact mk x

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : ↑I → X
hγ'F : ∀ (t : ↑I), γ' t ∈ F
hγ' : ∀ (t : ↑I), f (γ' t) = γ t
⊢ x ⤳ γ' 0

Tactic:
← hf.specializes_iff,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : ↑I → X
hγ'F : ∀ (t : ↑I), γ' t ∈ F
hγ' : ∀ (t : ↑I), f (γ' t) = γ t
⊢ f x ⤳ f (γ' 0)
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : ↑I → X
hγ'F : ∀ (t : ↑I), γ' t ∈ F
hγ' : ∀ (t : ↑I), f (γ' t) = γ t
h₀ : x ⤳ γ' 0
⊢ γ' 1 ⤳ y

Tactic:
← hf.specializes_iff,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : ↑I → X
hγ'F : ∀ (t : ↑I), γ' t ∈ F
hγ' : ∀ (t : ↑I), f (γ' t) = γ t
h₀ : x ⤳ γ' 0
⊢ f (γ' 1) ⤳ f 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),
    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:
intro K

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
⊢ 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
Module: Mathlib.Topology.Instances.Sign

Goal state before:
pp: α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableLT α
inst✝ : OrderTopology α
a : α
h : 0 < a
⊢ ∀ᶠ (x : α) in nhds a, 1 = SignType.sign x

Tactic:
eventually_nhds_iff

Goal state after:
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableLT α
inst✝ : OrderTopology α
a : α
h : 0 < a
⊢ ∃ t, (∀ y ∈ t, 1 = SignType.sign y) ∧ IsOpen t ∧ a ∈ t
Module: Mathlib.Topology.Instances.Sign

Goal state before:
pp: α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableLT α
inst✝ : OrderTopology α
a : α
h : a < 0
⊢ ∀ᶠ (x : α) in nhds a, -1 = SignType.sign x

Tactic:
eventually_nhds_iff

Goal state after:
α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableLT α
inst✝ : OrderTopology α
a : α
h : a < 0
⊢ ∃ t, (∀ y ∈ t, -1 = SignType.sign y) ∧ IsOpen t ∧ a ∈ t
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case refine_1.left
x r : ℝ
hr : ∀ (m : ℝ), ↑m = ↑x → r ≤ ‖m‖
⊢ r ≤ fract x

pp: case refine_1.right
x r : ℝ
hr : ∀ (m : ℝ), ↑m = ↑x → r ≤ ‖m‖
⊢ r ≤ 1 - fract x

Tactic:
· simpa [abs_of_nonneg] using hr (fract x)

Goal state after:
case refine_1.right
x r : ℝ
hr : ∀ (m : ℝ), ↑m = ↑x → r ≤ ‖m‖
⊢ r ≤ 1 - fract x
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr
p x ε : ℝ
hp : p ≠ 0
y : ℝ
n : ℤ
hn : |y - x - ↑n * p| ≤ ε
⊢ |y - x - ↑(round (p⁻¹ * (y - x))) * p| ≤ ε

Tactic:
← mul_le_mul_iff_right₀ (abs_pos.mpr <| inv_ne_zero hp),

Goal state after:
case inr
p x ε : ℝ
hp : p ≠ 0
y : ℝ
n : ℤ
hn : |p⁻¹| * |y - x - ↑n * p| ≤ |p⁻¹| * ε
⊢ |p⁻¹| * |y - x - ↑(round (p⁻¹ * (y - x))) * p| ≤ |p⁻¹| * ε
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ 0 ≤ arccos x

Tactic:
unfold arccos; linarith [arcsin_le_pi_div_two x]

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

Goal state before:
pp: x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
⊢ ∀ n ≥ ⌊‖x‖⌋₊, ‖x ^ (n + 1) / ↑(n + 1)!‖ ≤ ‖x‖ / (↑⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖

Tactic:
intro n hn

Goal state after:
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
⊢ ‖x ^ (n + 1) / ↑(n + 1)!‖ ≤ ‖x‖ / (↑⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ (cos ↑θ + sin ↑θ * I).arg = θ

Tactic:
rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I zero_lt_one hθ]

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

Goal state before:
pp: z : ℂ
⊢ (cexp z).arg = (cexp (↑z.re + ↑z.im * I)).arg

Tactic:
re_add_im

Goal state after:
z : ℂ
⊢ (cexp z).arg = (cexp z).arg
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
x✝ : x ∈ univ
⊢ log (-rexp x) = x

Tactic:
rw [log_neg_eq_log, log_exp]

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

Goal state before:
pp: x : ℂ
hx : x ≠ 0
⊢ ↑x.re + ↑x.im * I = x

Tactic:
re_add_im

Goal state after:
x : ℂ
hx : x ≠ 0
⊢ x = x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
⊢ ↑x.re + ↑x.im * I = x

Tactic:
re_add_im

Goal state after:
x : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
⊢ x = x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (2 • θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-π / 2) (π / 2)

Tactic:
by
  rw [two_zsmul, ← two_nsmul, two_nsmul_toReal_eq_two_mul]

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

Goal state before:
pp: x : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
⊢ arg =ᶠ[𝓝 x] fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π

Tactic:
suffices h_forall_nhds : ∀ᶠ y : ℂ in 𝓝 x, y.re < 0 ∧ 0 < y.im from
    h_forall_nhds.mono fun y hy => arg_of_re_neg_of_im_nonneg hy.1 hy.2.le

Goal state after:
x : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
⊢ ∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ 0 < y.im
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
hy : y ≠ 0
⊢ x ^ y ≠ 0 ↔ x ≠ 0

Tactic:
by
  simp [hx, hy]

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

Goal state before:
pp: x : ℝ
⊢ x ^ (log x)⁻¹ ≤ rexp 1

Tactic:
by
  calc
    _ ≤ |x ^ (log x)⁻¹| := le_abs_self _
    _ ≤ |x| ^ (log x)⁻¹ := abs_rpow_le_abs_rpow ..
  rw [← log_abs]
  obtain hx | hx := (abs_nonneg x).eq_or_lt'
  · simp [hx]
  · rw [rpow_def_of_pos hx]
    gcongr
    exact mul_inv_le_one

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

Goal state before:
pp: s : ℝ
n : ℕ
hn : s < ↑n
⊢ (fun x ↦ rexp x / x ^ n) ≤ᶠ[atTop] fun x ↦ rexp x / x ^ s

Tactic:
filter_upwards [eventually_gt_atTop (0 : ℝ), eventually_ge_atTop (1 : ℝ)] with x hx₀ hx₁

Goal state after:
s : ℝ
n : ℕ
hn : s < ↑n
x : ℝ
hx₀ : 0 < x
hx₁ : 1 ≤ x
⊢ rexp x / x ^ n ≤ rexp x / x ^ s
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ ↑(rexp (↑y * log x).re) * (↑(Real.cos (↑y * log x).im) + ↑(Real.sin (↑y * log x).im) * I) =
    ↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)

Tactic:
rw [re_ofReal_mul, im_ofReal_mul, log_re, log_im, mul_comm y, mul_comm y, Real.exp_mul,
      Real.exp_log]

Goal state after:
case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ 0 < ‖x‖
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
rcases eq_or_ne w.re 0 with hw | hw

Goal state after:
case inr.inl
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re = 0
⊢ ‖0 ^ w‖ = 0 ^ w.re / rexp (arg 0 * w.im)

case inr.inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ ‖0 ^ w‖ = 0 ^ w.re / rexp (arg 0 * w.im)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
y : ℝ
⊢ x ^ y = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
rw [← NNReal.coe_inj, coe_rpow, ← NNReal.coe_eq_zero]

Goal state after:
x : ℝ≥0
y : ℝ
⊢ ↑x ^ y = ↑0 ↔ ↑x = 0 ∧ y ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

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

Tactic:
by
  suffices ∀ᶠ x : ℂ in 𝓝 a, x ≠ 0 from
    this.mono fun x hx ↦ by
      dsimp only
      rw [cpow_def_of_ne_zero hx]
  exact IsOpen.eventually_mem isOpen_ne ha

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

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

Tactic:
← rpow_le_rpow_iff hx _ hz,

Goal state after:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ x ^ z ≤ (y ^ z⁻¹) ^ z ↔ x ^ z ≤ y

x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ 0 ≤ y ^ z⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : z ≠ 0
⊢ x ^ z⁻¹ = y ↔ x = y ^ z

Tactic:
rw [← rpow_left_inj _ hy hz, rpow_inv_rpow hx hz]; positivity

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

Goal state before:
pp: x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
h_one_le : 1 ≤ z
⊢ x ^ 1 ≤ x ^ z

Tactic:
exact ENNReal.rpow_le_rpow_of_exponent_le hx h_one_le

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

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

Tactic:
rw [sub_eq_add_neg, ← vadd_eq_add, ← vadd_eq_add, ← midpoint_vadd_midpoint]; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : M
c₁ c₂ : R
h : 0 ≤ c₁ * c₂
hc₁ : c₁ ≠ 0
hc₂ : c₂ = 0
⊢ SameRay R (c₁ • v) 0

Tactic:
exact SameRay.zero_right _

Goal state after:
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₁ → P₂
e' : V₁ ≃ₗ[k] V₂
p : P₁
h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p
q' : P₂
⊢ e ((fun q' ↦ e'.symm (q' -ᵥ e p) +ᵥ p) q') = q'

Tactic:
by simp [h (e'.symm (q' -ᵥ e p) +ᵥ p), vadd_vsub, vsub_vadd]

Goal state after:
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.symm.symm (e.linear.symm v +ᵥ e.symm p)

Tactic:
Equiv.symm_symm,

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 = e.toEquiv (e.linear.symm v +ᵥ e.symm p)
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : CommSemiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
c : 𝕜
⊢ StarConvex 𝕜 (z + c • x) ((fun x ↦ z + c • x) '' s)

Tactic:
have h := (hs.smul c).add_left z
  rwa [← image_smul, image_image] at h

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : AddRightMono 𝕜
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
⊢ MapsTo (⇑(AffineMap.lineMap x y)) (Icc 0 1) s

Tactic:
by
  simpa only [mapsTo_iff_image_subset, segment_eq_image_lineMap] using h.segment_subset hx hy

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

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
direction : Submodule k V
p₁ : P
hp₁ : p₁ ∈ mk' p direction
p₂ : P
hp₂ : p₂ ∈ mk' p direction
⊢ p₁ -ᵥ p₂ ∈ direction

Tactic:
simpa using direction.sub_mem hp₁ hp₂

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedRing 𝕜
inst✝ : SMul 𝕜 E
f : E → 𝕜
hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y
hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x
B : 𝕜
x : E
hx : x ∈ {x | f x ≤ B}
y : E
hy : y ∈ {x | f x ≤ B}
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hs : a + b = 1
⊢ a • x + b • y ∈ {x | f x ≤ B}

Tactic:
calc
    _ ≤ a • (f x) + b • (f y) := le_trans (hf1 _ _) (add_le_add (hf2 x ha) (hf2 y hb))
    _ ≤ a • B + b • B := by gcongr <;> assumption
    _ ≤ B := by rw [← add_smul, hs, one_smul]

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

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
x : E
hx : x ∉ (convexHull 𝕜) (s \ {x})
y : E
hy : y ∈ (convexHull 𝕜) (s \ {x})
⊢ y ∉ {x}

Tactic:
rintro (rfl : y = x)
        exact hx hy

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
inst✝ : AffineSpace V P
s : Set P
⊢ affineSpan k s ≠ ⊥ ↔ s ≠ ∅

Tactic:
← nonempty_iff_ne_bot,

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
⊢ (↑(affineSpan k s)).Nonempty ↔ s ≠ ∅
Module: Mathlib.Analysis.LocallyConvex.Bounded

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

Tactic:
rw [ht.absorbs_biUnion]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ ∃ r, ∀ x ∈ s, ‖x‖ ≤ r

Tactic:
NormedSpace.isVonNBounded_iff,

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsBounded s ↔ ∃ r, ∀ x ∈ s, ‖x‖ ≤ r
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
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 • max (f x) (g x) + b • max (f y) (g y)

Tactic:
gcongr <;> apply le_sup_left

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 : 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 • max (f x) (g x) + b • max (f y) (g y)

Tactic:
gcongr <;> apply le_sup_left

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
inst✝¹ : AffineSpace V P
A : Set P
inst✝ : Nonempty ↑A
⊢ affineSpan k (Subtype.val ⁻¹' A) = ⊤

Tactic:
rw [eq_top_iff]

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
A : Set P
inst✝ : Nonempty ↑A
⊢ ⊤ ≤ affineSpan k (Subtype.val ⁻¹' A)
Module: Mathlib.LinearAlgebra.AffineSpace.Combination

Goal state before:
pp: case 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 ι
w : ι → k
p : ι → P
h : ∑ i ∈ s, w i = 1
b₁ b₂ : P
| ∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂))

Tactic:
congr
      · skip
      · ext
        rw [← smul_sub, vsub_sub_vsub_cancel_left]

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 ι
inst✝ : DecidableEq ι
w : ι → k
p : ι → P
i : ι
⊢ ((insert i s).weightedVSubOfPoint p (p i)) w = (s.weightedVSubOfPoint p (p i)) w

Tactic:
rw [weightedVSubOfPoint_apply, weightedVSubOfPoint_apply]
  apply sum_insert_zero
  rw [vsub_self, smul_zero]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case cons
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
x : E
a : ι
s : Finset ι
ha : a ∉ s
ih : (s.sup p) x = ↑(s.sup fun i ↦ NNReal.mk ((p i) x) ⋯)
⊢ ((Finset.cons a s ha).sup p) x = ↑((Finset.cons a s ha).sup fun i ↦ NNReal.mk ((p i) x) ⋯)

Tactic:
| cons a s ha ih =>

Goal state after:
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)
x y : E
⊢ (⨆ p, ⇑↑p) (x + y) ≤ (⨆ p, ⇑↑p) x + (⨆ p, ⇑↑p) y

Tactic:
by
          rcases h with ⟨q, hq⟩
          obtain rfl | h := s.eq_empty_or_nonempty
          · simp [Real.iSup_of_isEmpty]
          have : Nonempty ↑s := h.coe_sort
          simp only [iSup_apply]
          refine ciSup_le fun i =>
            ((i : Seminorm 𝕜 E).add_le' x y).trans <| add_le_add
              -- Porting note: `f` is provided to force `Subtype.val` to appear.
              -- A type ascription on `_` would have also worked, but would have been more verbose.
              (le_ciSup (f := fun i => (Subtype.val i : Seminorm 𝕜 E).toFun x) ⟨q x, ?_⟩ i)
              (le_ciSup (f := fun i => (Subtype.val i : Seminorm 𝕜 E).toFun y) ⟨q y, ?_⟩ i)
          <;> rw [mem_upperBounds, forall_mem_range]
          <;> exact fun j => hq (mem_image_of_mem _ j.2) _

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

Goal state before:
pp: k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
inst✝ : DecidableEq ι
i j : ι
h : i ≠ j
c : k
⊢ affineCombinationLineMapWeights i j c i = 1 - c

Tactic:
by
  simp [affineCombinationLineMapWeights, h.symm, sub_eq_neg_add]

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case refine_1
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
hs₁ : BddAbove s
hs₂ : s.Nonempty
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
this : Nonempty ↑s
⊢ p x ≤ ⨆ i, ↑i x

Tactic:
rcases hs₁ with ⟨q, hq⟩
    exact le_ciSup ⟨q x, forall_mem_range.mpr fun i : s => hq i.2 x⟩ ⟨p, hp⟩

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

Goal state before:
pp: k : Type u_1
inst✝² : DivisionRing k
ι : Type u_4
s : Finset ι
inst✝¹ : CharZero k
inst✝ : Fintype ι
h : s.Nonempty
⊢ ∑ i, centroidWeightsIndicator k s i = 1

Tactic:
by
  rw [sum_centroidWeightsIndicator]
  exact s.sum_centroidWeights_eq_one_of_nonempty k h

Goal state after: