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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
hr : r ∈ closedBall 0 (ε / R)
y : E
hy : y ∈ (fun x_1 ↦ -x + x_1) ⁻¹' (r • s)
⊢ y ∈ u

Tactic:
obtain ⟨z, zs, hz⟩ : ∃ z : E, z ∈ s ∧ r • z = -x + y := by simpa [mem_smul_set] using hy

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
hr : r ∈ closedBall 0 (ε / R)
y : E
hy : y ∈ (fun x_1 ↦ -x + x_1) ⁻¹' (r • s)
z : E
zs : z ∈ s
hz : r • z = -x + y
⊢ y ∈ u
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : C(Y, Z)
hg : IsInducing ⇑g
⊢ compactOpen = induced g.comp compactOpen

Tactic:
by
    simp only [compactOpen_eq, induced_generateFrom_eq, image_image2, hg.setOfPred_isOpen,
      image2_image_right, MapsTo, mem_preimage, preimage_ofPred_eq, comp_apply]

Goal state after:
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)
hfm : Monotone f
k : ℕ
⊢ l ≤ ∑ i ∈ Finset.range (2 * k), (-1) ^ i * f i

Tactic:
have ha : Antitone (fun n ↦ ∑ i ∈ range (2 * n), (-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, one_mul,
      ← sub_eq_add_neg, sub_le_iff_le_add]
    gcongr
    exact hfm (by lia)
  exact ha.le_of_tendsto (hfl.comp (tendsto_atTop_mono (fun n ↦ by dsimp; lia) tendsto_id)) _

Goal state after:
Module: Mathlib.Topology.Path

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

Tactic:
min_eq_left this.2,

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

Goal state before:
pp: x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ π / 2 - arcsin (cos x) = x

Tactic:
← sin_pi_div_two_sub,

Goal state after:
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ π / 2 - arcsin (sin (π / 2 - x)) = x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ |log x * x| < 1

Tactic:
have aux : 0 ≤ -log x * x := by
    refine mul_nonneg ?_ h1.le
    rw [← log_inv]
    apply log_nonneg
    rw [← le_inv_comm₀ h1 zero_lt_one, inv_one]
    exact h2

Goal state after:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
aux : 0 ≤ -log x * x
⊢ |log x * x| < 1
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:
rw [← prod_map_toList, log_list_prod (by simp_all)]
  simp

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

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

pp: case convert_1
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ‖z‖ ≠ 0

Tactic:
· simp [sub_eq_add_neg]

Goal state after:
case convert_1
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ‖z‖ ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: y : ℝ
⊢ Tendsto (fun x ↦ log (x + y) - log x) atTop (𝓝 0)

Tactic:
have : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0)) :=
    tendsto_const_nhds.add (tendsto_const_nhds.div_atTop tendsto_id)

Goal state after:
y : ℝ
this : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
⊢ Tendsto (fun x ↦ log (x + y) - log x) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case pos
x y : ℂ
h✝¹ : x = 0
h✝ : y = 0
⊢ 1 = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
simp [*, exp_ne_zero]

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

Goal state before:
pp: case neg
x y : ℂ
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0 = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
simp [*, exp_ne_zero]

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

Goal state before:
pp: case neg
x y : ℂ
h✝ : ¬x = 0
⊢ cexp (log x * y) = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
simp [*, exp_ne_zero]

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

Goal state before:
pp: case mpr.inr
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * ↑k
⊢ sin θ = sin ψ

Tactic:
have H' : θ + ψ = 2 * k * π + π := by
      rwa [← sub_add, sub_add_eq_add_sub, sub_eq_iff_eq_add, mul_assoc, mul_comm π _, ←
        mul_assoc] at H

Goal state after:
case mpr.inr
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * ↑k
H' : θ + ψ = 2 * ↑k * π + π
⊢ sin θ = sin ψ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ Real.arcsin ((-z).im / ‖z‖) < π - π / 2

Tactic:
sub_half,

Goal state after:
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ Real.arcsin ((-z).im / ‖z‖) < π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ.sin ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑π

Tactic:
by
  rw [← not_or, ← sin_eq_zero_iff]

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

Goal state before:
pp: x : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
⊢ IsOpen fun y ↦ y.re < 0 ∧ 0 < y.im

Tactic:
exact
    IsOpen.and (isOpen_lt continuous_re continuous_zero) (isOpen_lt continuous_zero continuous_im)

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

Goal state before:
pp: ⊢ (↑π).tan = 0

Tactic:
by rw [tan_coe, Real.tan_pi]

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

Goal state before:
pp: a b : Angle
h : 2 • a = 2 • b
h_sign : a.sign = -b.sign
h_ne : b.sign ≠ 0
⊢ a = b + ↑π

Tactic:
by
  have h1 := Real.Angle.two_zsmul_eq_iff.mp h
  refine h1.resolve_left ?_
  rintro rfl
  simp only [SignType.self_eq_neg_iff] at h_sign
  rw [h_sign] at h_ne
  contradiction

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

Goal state before:
pp: case pos
x y : ℝ
hx : 0 ≤ x
h✝¹ : x = 0
h✝ : y = 0
⊢ 1 = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
simp [*, exp_ne_zero]

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

Goal state before:
pp: case neg
x y : ℝ
hx : 0 ≤ x
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ 0 = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
simp [*, exp_ne_zero]

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

Goal state before:
pp: case neg
x y : ℝ
hx : 0 ≤ x
h✝ : ¬x = 0
⊢ rexp (log x * y) = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
simp [*, exp_ne_zero]

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

Goal state before:
pp: case inr
x y : ℝ
hx : x < 0
⊢ |x ^ y| ≤ |x| ^ y

Tactic:
rw [abs_of_neg hx, rpow_def_of_neg hx, rpow_def_of_pos (neg_pos.2 hx), log_neg_eq_log, abs_mul,
      abs_of_pos (exp_pos _)]

Goal state after:
case inr
x y : ℝ
hx : x < 0
⊢ rexp (log x * y) * |cos (y * π)| ≤ rexp (log x * y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: ι : Type u_1
a : ℝ
ha : 0 ≤ a
s : Finset ι
f : ι → ℝ
h : ∀ x ∈ s, 0 ≤ f x
⊢ a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x

Tactic:
induction s using Finset.cons_induction with

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

Goal state before:
pp: case inr
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hf : 0 ≤ᶠ[l] f
hg : 0 ≤ᶠ[l] g
h : f =Θ[l] g
rpow_pos :
  ∀ {α : Type u_1} {r : ℝ} {l : Filter α} {f g : α → ℝ},
    0 ≤ᶠ[l] f → 0 ≤ᶠ[l] g → f =Θ[l] g → r ≥ 0 → (fun x ↦ f x ^ r) =Θ[l] fun x ↦ g x ^ r
hr : ¬r ≥ 0
⊢ (fun x ↦ (f x ^ r)⁻¹) =Θ[l] fun x ↦ (g x ^ r)⁻¹

Tactic:
grw [← EventuallyEq.isTheta <| hf.mono fun x hfx ↦ Real.rpow_neg hfx r]

Goal state after:
case inr
α : Type u_1
r : ℝ
l : Filter α
f g : α → ℝ
hf : 0 ≤ᶠ[l] f
hg : 0 ≤ᶠ[l] g
h : f =Θ[l] g
rpow_pos :
  ∀ {α : Type u_1} {r : ℝ} {l : Filter α} {f g : α → ℝ},
    0 ≤ᶠ[l] f → 0 ≤ᶠ[l] g → f =Θ[l] g → r ≥ 0 → (fun x ↦ f x ^ r) =Θ[l] fun x ↦ g x ^ r
hr : ¬r ≥ 0
⊢ (fun x ↦ f x ^ (-r)) =Θ[l] fun x ↦ (g x ^ r)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 < x
⊢ x ^ z < y ^ z

Tactic:
· rw [rpow_def_of_pos hx, rpow_def_of_pos (lt_trans hx hxy), exp_lt_exp]
    exact mul_lt_mul_of_pos_right (log_lt_log hx hxy) hz

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

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

Tactic:
rcases eq_bot_or_bot_lt x with (rfl | (h : 0 < x))
  · have : z ≠ 0 := by linarith
    simp [this]
  nth_rw 2 [← NNReal.rpow_one x]
  exact NNReal.rpow_le_rpow_of_exponent_ge h hx h_one_le

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

Goal state before:
pp: case inl.inl
y : ℝ
⊢ 0 ^ y = 0 ^ 0 ↔ y = 0 ∨ 0 = 1 ∨ 0 = 0 ∧ (y = 0 ↔ 0 = 0)

Tactic:
simp [zero_rpow_def]

Goal state after:
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 ↔ y ^ z < x

Tactic:
rw [← rpow_lt_rpow_iff_of_neg hy _ hz, rpow_inv_rpow _ hz.ne]

Goal state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 ≤ x

x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 < x ^ 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 ↔ y ^ z ≤ x

Tactic:
by
  rw [← rpow_le_rpow_iff_of_neg hy _ hz, rpow_inv_rpow _ hz.ne] <;> positivity

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

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

Tactic:
exact mul_le_mul_of_nonpos_left hyz (log_nonpos (le_of_lt hx0) hx1)

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

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

Tactic:
apply ContinuousAt.mul

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

case hg
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
A : ContinuousAt (fun p ↦ (-↑p.1, p.2)) (x, y)
⊢ ContinuousAt (fun p ↦ cexp (↑π * I * p.2)) (x, y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
y : ℝ
hy0 : 0 ≤ y
⊢ x ^ y = ∞ → x = ∞

Tactic:
simp +contextual [ENNReal.rpow_eq_top_iff, hy0.not_gt]

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

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

Tactic:
by
  obtain (rfl | hx') := eq_or_ne x 0
  · by_cases hy' : 0 < y
    · simp [ENNReal.zero_rpow_of_pos hyz, ENNReal.zero_rpow_of_pos hy']
    · have hz' : 0 < z := by linarith
      simp [ENNReal.zero_rpow_of_pos hyz, ENNReal.zero_rpow_of_pos hz']
  · rw [ENNReal.rpow_add _ _ hx' hx]

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

Goal state before:
pp: case neg
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : ¬x = 0
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
rw [coe_le_one_iff] at hx1
    simp [← coe_rpow_of_ne_zero h,
      NNReal.rpow_le_rpow_of_exponent_ge (bot_lt_iff_ne_bot.mpr h) hx1 hyz]

Goal state after:
Module: Mathlib.Algebra.Order.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : Semiring β
inst✝³ : PartialOrder β
inst✝² : Algebra α β
inst✝¹ : PosMulMono β
inst✝ : MulPosMono β
h : Monotone ⇑(algebraMap α β)
⊢ Monotone fun x ↦ x • 1

Tactic:
by simpa [Algebra.smul_def] using h

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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
hx : x ≠ 0
⊢ rayOfNeZero R x hx ≠ -rayOfNeZero R x hx

Tactic:
neg_rayOfNeZero,

Goal state after:
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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
x : M
hx : x ≠ 0
⊢ rayOfNeZero R x hx ≠ rayOfNeZero R (-x) ⋯
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
⊢ (lineMap p₀ p₁) (1 - c) = (lineMap p₁ p₀) c

Tactic:
lineMap_symm p₀,

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₀).comp (lineMap 1 0)) (1 - c) = (lineMap p₁ p₀) c
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ (∃ a b, 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x) → x ∈ openSegment 𝕜 y z

Tactic:
rintro ⟨a, b, ha, hb, rfl⟩

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
⊢ (a / (a + b)) • y + (b / (a + b)) • z ∈ openSegment 𝕜 y z
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
f : E →ᵃ[𝕜] F
s : Set E
hs : StarConvex 𝕜 x s
y : F
y' : E
hy' : y' ∈ s
hy'f : f y' = y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y' = a • f x + b • y

Tactic:
hy'f

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
f : E →ᵃ[𝕜] F
s : Set E
hs : StarConvex 𝕜 x s
y : F
y' : E
hy' : y' ∈ s
hy'f : f y' = y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • y = a • f x + b • y
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: case inr
𝕜 : 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
s : Set E
hs : s.OrdConnected
h : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hyx : y ≤ x
⊢ [x -[𝕜] y] ⊆ s

Tactic:
rw [segment_symm]

Goal state after:
case inr
𝕜 : 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
s : Set E
hs : s.OrdConnected
h : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hyx : y ≤ x
⊢ [y -[𝕜] x] ⊆ s
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕜'
inst✝⁶ : NormedAlgebra 𝕜 𝕜'
inst✝⁵ : Nontrivial 𝕜'
inst✝⁴ : Zero E
inst✝³ : TopologicalSpace E
inst✝² : SMul 𝕜 E
inst✝¹ : MulAction 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
V : Set E
hV : V ∈ 𝓝 0
⊢ Absorbs 𝕜 V s

Tactic:
refine (h hV).restrict_scalars <| AntilipschitzWith.tendsto_cobounded (K := ‖(1 : 𝕜')‖₊⁻¹) ?_

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕜'
inst✝⁶ : NormedAlgebra 𝕜 𝕜'
inst✝⁵ : Nontrivial 𝕜'
inst✝⁴ : Zero E
inst✝³ : TopologicalSpace E
inst✝² : SMul 𝕜 E
inst✝¹ : MulAction 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
V : Set E
hV : V ∈ 𝓝 0
⊢ AntilipschitzWith ‖1‖₊⁻¹ fun x ↦ x • 1
Module: Mathlib.Topology.MetricSpace.Equicontinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
⊢ UniformEquicontinuous F

Tactic:
Metric.uniformEquicontinuous_iff

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
⊢ ∀ ε > 0, ∃ δ > 0, ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: case e'_5
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h : s.Pairwise fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s
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 = a / (a + b)

Tactic:
rw [hab, div_one]

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

Goal state before:
pp: case e'_6
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h : s.Pairwise fun x y ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s
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
⊢ b = b / (a + b)

Tactic:
rw [hab, div_one]

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
Q : AffineSubspace k P
p₀ p₁ : P
c : k
h₀ : p₀ ∈ Q
h₁ : p₁ ∈ Q
⊢ (lineMap p₀ p₁) c ∈ Q

Tactic:
AffineMap.lineMap_apply

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
Q : AffineSubspace k P
p₀ p₁ : P
c : k
h₀ : p₀ ∈ Q
h₁ : p₁ ∈ Q
⊢ c • (p₁ -ᵥ p₀) +ᵥ p₀ ∈ Q
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
r : k
hr : r • (p₂ -ᵥ p₁) = p -ᵥ p₁
⊢ (AffineMap.lineMap p₁ p₂) r = r • (p₂ -ᵥ p₁) +ᵥ p₁

Tactic:
AffineMap.lineMap_apply

Goal state after:
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
r : k
hr : r • (p₂ -ᵥ p₁) = p -ᵥ p₁
⊢ r • (p₂ -ᵥ p₁) +ᵥ p₁ = r • (p₂ -ᵥ p₁) +ᵥ 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
h : ∑ i ∈ s, w i = 1
b₁ b₂ : P
⊢ b₁ -ᵥ b₂ + (b₂ -ᵥ b₁) = 0

Tactic:
vsub_add_vsub_cancel,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
h : ∑ i ∈ s, w i = 1
b₁ b₂ : P
⊢ b₁ -ᵥ b₁ = 0
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 ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
w₁ w₂ : ι → k
⊢ (s.weightedVSubOfPoint p (Classical.choice ⋯)) (w₂ +ᵥ w₁) +ᵥ Classical.choice ⋯ =
    (s.weightedVSub p) w₂ +ᵥ (s.weightedVSubOfPoint p (Classical.choice ⋯)) w₁ +ᵥ Classical.choice ⋯

Tactic:
by simp_rw [vadd_vadd, weightedVSub, vadd_eq_add, map_add]

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) ⋯)
⊢ max ((p a) x) ((s.sup p) x) = max ↑(NNReal.mk ((p a) x) ⋯) ↑(s.sup fun i ↦ NNReal.mk ((p i) x) ⋯)

Tactic:
NNReal.coe_mk,

Goal state after:
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) ⋯)
⊢ max ((p a) x) ((s.sup p) x) = max ((p a) x) ↑(s.sup fun i ↦ NNReal.mk ((p i) x) ⋯)
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
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 : AffineSubspace k P₁
h : ⇑f '' ↑s = ∅
⊢ s = ⊥

Tactic:
image_eq_empty,

Goal state after:
case refine_1
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 : AffineSubspace k P₁
h : ↑s = ∅
⊢ s = ⊥
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : Seminorm 𝕜 E
x✝ : E
⊢ (r • (p ⊓ q)) x✝ = (r • p ⊓ r • q) x✝

Tactic:
simp_rw [smul_apply, inf_apply, smul_apply, ← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def,
    smul_eq_mul, Real.mul_iInf_of_nonneg (NNReal.coe_nonneg _), mul_add]

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

Goal state before:
pp: k : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
inst✝² : AddCommGroup W
inst✝¹ : Module k W
inst✝ : AffineSpace W Q
s : Set P
t : Set Q
⊢ vectorSpan k (s ×ˢ t) ≤ (vectorSpan k s).prod (vectorSpan k t)

Tactic:
simpa [vectorSpan_def, Set.prod_vsub_prod_comm] using Submodule.span_prod_le (s -ᵥ s) (t -ᵥ t)

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 ι
p : ι → P
i j : ι
hi : i ∈ s
hj : j ∈ s
c : k
⊢ c • (p j -ᵥ p i) +ᵥ p i = (AffineMap.lineMap (p i) (p j)) c

Tactic:
AffineMap.lineMap_apply

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
p : ι → P
i j : ι
hi : i ∈ s
hj : j ∈ s
c : k
⊢ c • (p j -ᵥ p i) +ᵥ p i = c • (p j -ᵥ p i) +ᵥ p i
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ : ℝ
hr₁ : r₁ ≠ 0
r₂ : ℝ
⊢ Metric.closedBall 0 r₁ • p.ball 0 r₂ ⊆ p.ball 0 (r₁ * r₂)

Tactic:
simp only [smul_subset_iff, mem_ball_zero, mem_closedBall_zero_iff, map_smul_eq_mul]

Goal state after:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ : ℝ
hr₁ : r₁ ≠ 0
r₂ : ℝ
⊢ ∀ (a : 𝕜), ‖a‖ ≤ r₁ → ∀ (b : E), p b < r₂ → ‖a‖ * p b < r₁ * r₂