mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : LocallyCompactPair X Y
⊢ ∀ (x : C(X, Y) × X), Tendsto (fun fx ↦ fx.1 fx.2) (𝓝 x) (𝓝 (x.1 x.2))

Tactic:
(nhds_basis_opens _).tendsto_right_iff

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✝ : LocallyCompactPair X Y
⊢ ∀ (x : C(X, Y) × X) (i : Set Y), x.1 x.2 ∈ i ∧ IsOpen[inst✝³] i → ∀ᶠ (x : C(X, Y) × X) in 𝓝 x, x.1 x.2 ∈ i
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ mk y ∈ {mk x} ↔ y ∈ pathComponent x

Tactic:
mem_singleton_iff,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ mk y = mk x ↔ y ∈ pathComponent x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
hx : x ≠ 0
⊢ Real.cos x.arg = x.re / ‖x‖

Tactic:
rw [arg]
  split_ifs with h₁ h₂
  · rw [Real.cos_arcsin]
    field_simp
    simp [Real.sqrt_sq, (norm_pos_iff.mpr hx).le, *]
    field
  · rw [Real.cos_add_pi, Real.cos_arcsin]
    field_simp
    simp [Real.sqrt_div (sq_nonneg _), Real.sqrt_sq_eq_abs, _root_.abs_of_neg (not_le.1 h₁), *]
    field
  · rw [Real.cos_sub_pi, Real.cos_arcsin]
    field_simp
    simp [Real.sqrt_div (sq_nonneg _), Real.sqrt_sq_eq_abs, _root_.abs_of_neg (not_le.1 h₁), *]
    field

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ 1 + x = (2 + 2 * x / (x + 2)) / (2 - 2 * x / (x + 2))

pp: x : ℝ
hx : 0 ≤ x
⊢ 2 * x / (x + 2) < 2

Tactic:
all_goals field_simp; grind

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

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ 1 + x = (2 + 2 * x / (x + 2)) / (2 - 2 * x / (x + 2))

pp: x : ℝ
hx : 0 < x
⊢ 2 * x / (x + 2) < 2

Tactic:
all_goals field_simp; grind

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

Goal state before:
pp: ψ θ : Angle
this : Int.natAbs 2 = 2
⊢ 2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑π

Tactic:
rw [zsmul_eq_iff two_ne_zero, this, Fin.exists_fin_two, Fin.val_zero,
    Fin.val_one, zero_smul, add_zero, one_smul, Int.cast_two,
    mul_div_cancel_left₀ (_ : ℝ) two_ne_zero]

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

Goal state before:
pp: θ : Angle
⊢ 2 • θ = ↑π ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)

Tactic:
rw [two_zsmul, ← two_nsmul, two_nsmul_eq_pi_iff]

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

Goal state before:
pp: x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
by
  simp only [cpow_def]
  split_ifs <;> simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

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

Goal state before:
pp: case inl.inr.inl
n : ℤ
hn : n ≠ 0
⊢ 0 ^ (↑n * 0) = (0 ^ 0) ^ n

Tactic:
simp [*, zero_zpow]

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

Goal state before:
pp: case inl.inr.inr
n : ℤ
y : ℂ
hn : n ≠ 0
hy : y ≠ 0
⊢ 0 ^ (↑n * y) = (0 ^ y) ^ n

Tactic:
simp [*, zero_zpow]

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

Goal state before:
pp: case inr.inr.inr.inl
x : ℂ
hr : 0 < x.re
hi : x.im = 0
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π

pp: case inr.inr.inr.inr
x : ℂ
hr : 0 < x.re
hi : 0 < x.im
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π

Tactic:
· simp [hr.le, hr.le.not_gt]

Goal state after:
case inr.inr.inr.inr
x : ℂ
hr : 0 < x.re
hi : 0 < x.im
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inr.inr.inr
x : ℂ
hr : 0 < x.re
hi : 0 < x.im
⊢ (if 0 ≤ x.re then -Real.arcsin (x.im / ‖x‖)
    else if 0 ≤ -x.im then Real.arcsin (x.im / ‖x‖) + π else Real.arcsin (x.im / ‖x‖) - π) =
    if x.re < 0 ∧ x.im = 0 then π
    else
      -if 0 ≤ x.re then Real.arcsin (x.im / ‖x‖)
        else if 0 ≤ x.im then -Real.arcsin (x.im / ‖x‖) + π else -Real.arcsin (x.im / ‖x‖) - π

Tactic:
· simp [hr.le, hr.le.not_gt]

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

Goal state before:
pp: case h.h
x✝¹ x✝ : ℝ
h : 2 • ↑x✝¹ + 2 • ↑x✝ = ↑π
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹

Tactic:
rw [← smul_add, ← coe_add, ← coe_nsmul, two_nsmul, ← two_mul, angle_eq_iff_two_pi_dvd_sub] at h

Goal state after:
case h.h
x✝¹ x✝ : ℝ
h : ∃ k, 2 * (x✝¹ + x✝) - π = 2 * π * ↑k
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ.toReal < 0 ↔ θ.sign = -1

Tactic:
rw [sign, ← sin_toReal, sign_eq_neg_one_iff]

Goal state after:
θ : Angle
⊢ θ.toReal < 0 ↔ Real.sin θ.toReal < 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mpr
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
⊢ a = b → a = b ∨ a = b + ↑π

Tactic:
intro h
    aesop

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

Goal state before:
pp: case cons
ι : Type u_1
a : ℝ
ha : 0 ≤ a
f : ι → ℝ
i : ι
s : Finset ι
hi : i ∉ s
ihs : (∀ x ∈ s, 0 ≤ f x) → a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x
h : ∀ x ∈ cons i s hi, 0 ≤ f x
⊢ a ^ ∑ x ∈ cons i s hi, f x = ∏ x ∈ cons i s hi, a ^ f x

Tactic:
| cons i s hi ihs =>

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

Goal state before:
pp: case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
hne : ↑x ≠ 0
⊢ ↑x ^ y = (-↑x) ^ y * cexp (↑π * I * y)

Tactic:
cpow_def_of_ne_zero hne,

Goal state after:
case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
hne : ↑x ≠ 0
⊢ cexp (log ↑x * y) = (-↑x) ^ y * cexp (↑π * I * y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: h : Tendsto (fun x ↦ log x * x) (𝓝[>] 0) (𝓝 0)
h_eq : ∀ x ∈ Set.Iio 0, (-(fun x ↦ log x * x) ∘ fun x ↦ |x|) x = log x * x
⊢ Tendsto (-(fun x ↦ log x * x) ∘ fun x ↦ |x|) (𝓝[<] 0) (𝓝 0)

Tactic:
nth_rewrite 3 [← neg_zero]

Goal state after:
h : Tendsto (fun x ↦ log x * x) (𝓝[>] 0) (𝓝 0)
h_eq : ∀ x ∈ Set.Iio 0, (-(fun x ↦ log x * x) ∘ fun x ↦ |x|) x = log x * x
⊢ Tendsto (-(fun x ↦ log x * x) ∘ fun x ↦ |x|) (𝓝[<] 0) (𝓝 (-0))
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

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

Tactic:
obtain hx | rfl := ne_or_eq x 0

Goal state after:
case inl
x y : ℝ
hp : 0 < y
hx : x ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) (x, y)

case inr
y : ℝ
hp : 0 < y
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) (0, y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ log x * y < log x * z

Tactic:
exact mul_lt_mul_of_pos_left hyz (log_pos hx)

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

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

Tactic:
by
  convert! rpow_lt_rpow_of_exponent_gt hx1 hx2 hz
  exact (rpow_zero x).symm

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

Goal state before:
pp: 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)
⊢ 0 < (-↑(x, y).1, (x, y).2).1.re

Tactic:
rwa [neg_re, ofReal_re, neg_pos]

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
⊢ ContinuousAt (fun p ↦ ↑p.1 ^ p.2) (x, y)

Tactic:
· -- x < 0 : difficult case
    suffices ContinuousAt (fun p => (-(p.1 : ℂ)) ^ p.2 * exp (π * I * p.2) : ℝ × ℂ → ℂ) (x, y) by
      refine this.congr (eventually_of_mem (prod_mem_nhds (Iio_mem_nhds hx) univ_mem) ?_)
      exact fun p hp => (ofReal_cpow_of_nonpos (le_of_lt hp.1) p.2).symm
    have A : ContinuousAt (fun p => ⟨-↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) (x, y) := by fun_prop
    apply ContinuousAt.mul
    · refine (continuousAt_cpow (Or.inl ?_)).comp A
      rwa [neg_re, ofReal_re, neg_pos]
    · fun_prop

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

Goal state before:
pp: case inr
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
⊢ x⁻¹ ^ y = (x ^ y)⁻¹

Tactic:
rcases eq_or_ne x 0 with (rfl | h0)

Goal state after:
case inr.inl
y : ℝ
hy : y < 0 ∨ 0 < y
⊢ 0⁻¹ ^ y = (0 ^ y)⁻¹

case inr.inr
x : ℝ≥0∞
y : ℝ
hy : y < 0 ∨ 0 < y
h0 : x ≠ 0
⊢ x⁻¹ ^ y = (x ^ y)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
simp [← coe_rpow_of_ne_zero (ne_of_gt hx1),
    NNReal.one_le_rpow_of_pos_of_le_one_of_nonpos hx1 hx2 (le_of_lt hz)]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_1
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
h : SameRay R x y ∨ SameRay R x (-y)
⊢ ∃ g, ∑ i, g i • ![x, y] i = 0 ∧ ∃ i, g i ≠ 0

Tactic:
rcases h with ((hx0 | hy0 | ⟨r₁, r₂, hr₁, _, h⟩) | (hx0 | hy0 | ⟨r₁, r₂, hr₁, _, h⟩))
    · exact False.elim (hx hx0)
    · exact False.elim (hy hy0)
    · refine ⟨![r₁, -r₂], ?_⟩
      rw [Fin.sum_univ_two, Fin.exists_fin_two]
      simp [h, hr₁.ne.symm]
    · exact False.elim (hx hx0)
    · exact False.elim (hy (neg_eq_zero.1 hy0))
    · refine ⟨![r₁, r₂], ?_⟩
      rw [Fin.sum_univ_two, Fin.exists_fin_two]
      simp [h, hr₁.ne.symm]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr.refine_1
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ r₂ / (r₁ + r₂) + r₁ / (r₁ + r₂) = 1

Tactic:
← add_div,

Goal state after:
case inr.inr.refine_1
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ (r₂ + r₁) / (r₁ + r₂) = 1
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case mp
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
hx : x ≠ 0
r : R
hr : 0 < r
⊢ SameRay R x (r • x) ∧ r • x ≠ 0

Tactic:
simp [hx, hr.le, hr.ne']

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hxy : SameRay R x y
hy : y ≠ 0
⊢ ∃ r, 0 < r ∧ r • x = y

Tactic:
exact (exists_pos_left_iff_sameRay hx hy).2 hxy

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Ring 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Invertible 2
x y : E
⊢ x ∈ openSegment 𝕜 (x - y) (x + y)

Tactic:
convert! midpoint_mem_openSegment (𝕜 := 𝕜) (x - y) (x + y)

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Ring 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Invertible 2
x y : E
⊢ x = midpoint 𝕜 (x - y) (x + y)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝³ : CommRing k
inst✝² : AddCommGroup V1
inst✝¹ : AffineSpace V1 P1
inst✝ : Module k V1
c p q : P1
r₁ r₂ : k
h : r₁ * r₂ = 1
h' : r₂ * r₁ = 1
⊢ (homothety c r₁) p = q ↔ (homothety c r₂) q = p

Tactic:
refine ⟨fun h1 ↦ ?_, fun h1 ↦ ?_⟩

Goal state after:
case refine_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝³ : CommRing k
inst✝² : AddCommGroup V1
inst✝¹ : AffineSpace V1 P1
inst✝ : Module k V1
c p q : P1
r₁ r₂ : k
h : r₁ * r₂ = 1
h' : r₂ * r₁ = 1
h1 : (homothety c r₁) p = q
⊢ (homothety c r₂) q = p

case refine_2
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝³ : CommRing k
inst✝² : AddCommGroup V1
inst✝¹ : AffineSpace V1 P1
inst✝ : Module k V1
c p q : P1
r₁ r₂ : k
h : r₁ * r₂ = 1
h' : r₂ * r₁ = 1
h1 : (homothety c r₂) q = p
⊢ (homothety c r₁) p = q
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
y z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ a / (a + b) + b / (a + b) = 1

Tactic:
← add_div,

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
hab : 0 < a + b
⊢ (a + b) / (a + b) = 1
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
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 0 < a + b
⊢ a / (a + b) + b / (a + b) = 1

Tactic:
← add_div,

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
hab : 0 < a + b
⊢ (a + b) / (a + b) = 1
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x y : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 y t
⊢ StarConvex 𝕜 (x + y) (s + t)

Tactic:
rw [← add_image_prod]
  exact (hs.prod ht).is_linear_image IsLinearMap.isLinearMap_add

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

Goal state before:
pp: case inr.refine_1
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
⊢ (y - z) / (y - x) + (z - x) / (y - x) = 1

Tactic:
← add_div,

Goal state after:
case inr.refine_1
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
⊢ (y - z + (z - x)) / (y - x) = 1
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case inr.refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
⊢ (y - z) * x / (y - x) + (z - x) * y / (y - x) = z

Tactic:
← add_div,

Goal state after:
case inr.refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
⊢ ((y - z) * x + (z - x) * y) / (y - x) = z
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 y t
⊢ StarConvex 𝕜 (x - y) (s - t)

Tactic:
by
  simp_rw [sub_eq_add_neg]
  exact hs.add ht.neg

Goal state after:
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 t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
⊢ Convex 𝕜 (s + t)

Tactic:
rw [← add_image_prod]
  exact (hs.prod ht).is_linear_image IsLinearMap.isLinearMap_add

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
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : (↑s₁ ∩ ↑s₂).Nonempty
p : P
hq1 : hn.some ∈ ↑s₁
hq2 : hn.some ∈ ↑s₂
hp : p ∈ s₁
⊢ p -ᵥ hn.some ∈ s₁.direction

Tactic:
exact vsub_mem_direction hp hq1

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Balanced 𝕜 s
ht : Balanced 𝕜 t
⊢ Balanced 𝕜 (s - t)

Tactic:
by
  simp_rw [sub_eq_add_neg]
  exact hs.add ht.neg

Goal state after:
Module: Mathlib.Topology.Algebra.UniformConvergence

Goal state before:
pp: α : Type u_1
G : Type u_2
ι : Type u_3
inst✝² : Group G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
𝔖 : Set (Set α)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) 𝔖
p : ι → Prop
b : ι → Set G
h : (𝓝 1).HasBasis p b
⊢ (𝓝 1).HasBasis (fun Si ↦ Si.1 ∈ 𝔖 ∧ p Si.2) fun Si ↦ {f | ∀ x ∈ Si.1, (toFun 𝔖) f x ∈ b Si.2}

Tactic:
convert!
    UniformOnFun.hasBasis_nhds_of_basis α _ 𝔖 (1 : α →ᵤ[𝔖] G) h𝔖₁ h𝔖₂ <|
      h.uniformity_of_nhds_one_swapped

Goal state after:
α : Type u_1
G : Type u_2
ι : Type u_3
inst✝² : Group G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
𝔖 : Set (Set α)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) 𝔖
p : ι → Prop
b : ι → Set G
h : (𝓝 1).HasBasis p b
x✝¹ : Set α × ι
x✝ : α →ᵤ[𝔖] G
⊢ (∀ x ∈ x✝¹.1, (toFun 𝔖) x✝ x ∈ b x✝¹.2) ↔ (x✝, 1) ∈ UniformOnFun.gen 𝔖 x✝¹.1 {x | x.1 / x.2 ∈ b x✝¹.2}
Module: Mathlib.Topology.Algebra.Equicontinuity

Goal state before:
pp: ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁷ : TopologicalSpace G
inst✝⁶ : UniformSpace M
inst✝⁵ : Group G
inst✝⁴ : Group M
inst✝³ : IsTopologicalGroup G
inst✝² : IsUniformGroup M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : EquicontinuousAt (DFunLike.coe ∘ F) 1
⊢ Equicontinuous (DFunLike.coe ∘ F)

Tactic:
rw [equicontinuous_iff_continuous]

Goal state after:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁷ : TopologicalSpace G
inst✝⁶ : UniformSpace M
inst✝⁵ : Group G
inst✝⁴ : Group M
inst✝³ : IsTopologicalGroup G
inst✝² : IsUniformGroup M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : EquicontinuousAt (DFunLike.coe ∘ F) 1
⊢ Continuous (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F))
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
ι₂ : Type u_5
s₂ : Finset ι₂
e : ι₂ ↪ ι
w : ι → k
p : ι → P
b : P
⊢ ∑ i ∈ map e s₂, w i • (p i -ᵥ b) = ∑ i ∈ s₂, (w ∘ ⇑e) i • ((p ∘ ⇑e) i -ᵥ b)

Tactic:
exact Finset.sum_map _ _ _

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₁ = (fun x ↦ x -ᵥ p₁) p₃ ∧ p₃ -ᵥ p₁ ∈ s₂.direction ⊔ k ∙ (p₂ -ᵥ p₁)

Tactic:
use rfl

Goal state after:
case right
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₁)
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
f : E → ℝ
map_zero : f 0 = 0
add_le : ∀ (x y : E), f (x + y) ≤ f x + f y
smul_le : ∀ (r : 𝕜) (x : E), f (r • x) ≤ ‖r‖ * f x
r : 𝕜
x : E
⊢ f (r • x) = ‖r‖ * f x

Tactic:
refine le_antisymm (smul_le r x) ?_
    by_cases h : r = 0
    · simp [h, map_zero]
    rw [← mul_le_mul_iff_right₀ (inv_pos.mpr (norm_pos_iff.mpr h))]
    rw [inv_mul_cancel_left₀ (norm_ne_zero_iff.mpr h)]
    specialize smul_le r⁻¹ (r • x)
    rw [norm_inv] at smul_le
    convert! smul_le
    simp [h]

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

Goal state before:
pp: case refine_2
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₂
⊢ k ∙ (p₂ -ᵥ p₁) ≤ (s₁ ⊔ s₂).direction

Tactic:
rw [direction_eq_vectorSpan, vectorSpan_def]

Goal state after:
case refine_2
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₂
⊢ k ∙ (p₂ -ᵥ p₁) ≤ Submodule.span k (↑(s₁ ⊔ s₂) -ᵥ ↑(s₁ ⊔ 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✝⁵ : SeminormedRing 𝕜
inst✝⁴ : AddGroup E
inst✝³ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x : E
r✝ : ℝ
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : Seminorm 𝕜 E
x✝¹ : 𝕜
x✝ : E
⊢ ↑(r • 1) * (‖x✝¹‖ * p x✝) = ‖x✝¹‖ * (↑(r • 1) * p x✝)

Tactic:
mul_left_comm

Goal state after:
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✝⁵ : SeminormedRing 𝕜
inst✝⁴ : AddGroup E
inst✝³ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x : E
r✝ : ℝ
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : Seminorm 𝕜 E
x✝¹ : 𝕜
x✝ : E
⊢ ‖x✝¹‖ * (↑(r • 1) * p x✝) = ‖x✝¹‖ * (↑(r • 1) * p x✝)
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ a / (a + b) + b / (a + b) = 1

Tactic:
← add_div,

Goal state after:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ (a + b) / (a + b) = 1