mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
f : Y → Path x y
g : Y → Path y z
⊢ Continuous[inst✝, _] f → Continuous[inst✝, _] g → Continuous[inst✝, _] fun t ↦ (f t).trans (g t)

Tactic:
intro hf hg
  apply continuous_uncurry_iff.mp
  exact trans_continuous_family _ (continuous_uncurry_iff.mpr hf) _ (continuous_uncurry_iff.mpr hg)

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ✝ : Path x y
a b : X
γ : Path a b
⊢ γ.extend 0 = a

Tactic:
γ.extend_zero

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ✝ : Path x y
a b : X
γ : Path a b
⊢ a = a
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
⊢ (γ.truncate 0 1) x = γ x

Tactic:
rw [truncate, coe_mk_mk, max_eq_left this.1, min_eq_left this.2, extend_extends']

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
r : R
hr : 0 < r
k m n : ℤ
h : r * ↑k ∈ Set.Ioo (r * ↑(m - 1)) (r * ↑(n + 1))
⊢ k ∈ Finset.Icc m n

Tactic:
simp only [Set.mem_Ioo, mul_lt_mul_iff_right₀ hr, Int.cast_lt] at h
  grind [Int.lt_iff_add_one_le]

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

Goal state before:
pp: x : ℝ
h : 0 < x
⊢ log x < 0 ↔ x < 1

Tactic:
rw [← log_one]
  exact log_lt_log_iff h zero_lt_one

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

Goal state before:
pp: ψ θ : ℝ
⊢ ↑θ = ↑ψ ↔ ∃ k, θ - ψ = 2 * π * ↑k

Tactic:
simp only [eq_comm]

Goal state after:
ψ θ : ℝ
⊢ ↑ψ = ↑θ ↔ ∃ k, θ - ψ = 2 * π * ↑k
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ ≠ -θ ↔ ¬(θ = 0 ∨ θ = ↑π)

Tactic:
← eq_neg_self_iff.not

Goal state after:
θ : Angle
⊢ θ ≠ -θ ↔ ¬θ = -θ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
rw [← not_or, ← eq_neg_self_iff.not]

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

Goal state before:
pp: x : ℂ
n : ℕ
h₀ : n ≠ 0
hlt : -(π / ↑n) < x.arg
hle : x.arg ≤ π / ↑n
⊢ (x ^ n) ^ (↑n)⁻¹ = x

Tactic:
rw [← cpow_nat_mul', mul_inv_cancel₀ (Nat.cast_ne_zero.2 h₀), cpow_one]
  · rwa [← div_lt_iff₀' (Nat.cast_pos.2 h₀.bot_lt), neg_div]
  · rwa [← le_div_iff₀' (Nat.cast_pos.2 h₀.bot_lt)]

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

Goal state before:
pp: case inr.inr
z : ℂ
hre : 0 < z.re
⊢ (0 ≤ z.re ∨ 0 ≤ z.im) ∧ ¬(z.re = 0 ∧ z.im < 0) ↔ 0 < z.re ∨ 0 ≤ z.im

Tactic:
simp [hre, hre.le, hre.ne']

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

Goal state before:
pp: case inr.inr
z : ℂ
hre : 0 < z.re
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

Tactic:
simp [hre, hre.le, hre.ne']

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

Goal state before:
pp: z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto arg (𝓝[{z | z.im < 0}] z) (𝓝 (-π))

Tactic:
suffices H : Tendsto (fun x : ℂ => Real.arcsin ((-x).im / ‖x‖) - π)
      (𝓝[{ z : ℂ | z.im < 0 }] z) (𝓝 (-π)) by
    refine H.congr' ?_
    have : ∀ᶠ x : ℂ in 𝓝 z, x.re < 0 := continuous_re.tendsto z (gt_mem_nhds hre)
    filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds this] with _ him hre
    rw [arg, if_neg hre.not_ge, if_neg him.not_ge]
  convert!
    (Real.continuousAt_arcsin.comp_continuousWithinAt
          ((continuous_im.continuousAt.comp_continuousWithinAt continuousWithinAt_neg).div
            continuous_norm.continuousWithinAt _)).sub_const
      π using 1
  · simp [him]
  · lift z to ℝ using him
    simpa using hre.ne

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

Goal state before:
pp: x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z ↦ ↑z.arg + ↑π

Tactic:
rw [Function.update_eq_iff]

Goal state after:
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ↑π = ↑(arg 0) + ↑π ∧ ∀ (x : ℂ), x ≠ 0 → ((Real.Angle.coe ∘ arg) ∘ Neg.neg) x = ↑x.arg + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: y : ℝ
hr : y < 0
⊢ Tendsto (fun x ↦ x ^ y) (𝓝[>] 0) atTop

Tactic:
simp_rw +singlePass [← neg_neg y, Real.rpow_neg_eq_inv_rpow]

Goal state after:
y : ℝ
hr : y < 0
⊢ Tendsto (fun x ↦ x⁻¹ ^ (-y)) (𝓝[>] 0) atTop
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case neg
x a : ℝ
hyp : (0 ^ ↑x).re = a
h : ¬x = 0
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
· rw [Complex.zero_cpow (Complex.ofReal_ne_zero.mpr h)] at hyp
      exact Or.inl ⟨h, hyp.symm⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
f : α → Angle
s : Set α
hf : ContinuousOn f s
hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑π
θ : Angle
hθ : θ ∈ f '' s
⊢ ContinuousAt sign θ

Tactic:
obtain ⟨z, hz, rfl⟩ := hθ

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
f : α → Angle
s : Set α
hf : ContinuousOn f s
hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑π
z : α
hz : z ∈ s
⊢ ContinuousAt sign (f z)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
n : ℕ
hx : 0 ≤ x
h : y + ↑n ≠ 0
⊢ x ^ y * x ^ ↑n = x ^ y * x ^ n

Tactic:
rpow_natCast

Goal state after:
x y : ℝ
n : ℕ
hx : 0 ≤ x
h : y + ↑n ≠ 0
⊢ x ^ y * x ^ n = x ^ y * x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
n : ℕ
hx : 0 ≤ x
h : y - ↑n ≠ 0
⊢ x ^ y / x ^ ↑n = x ^ y / x ^ n

Tactic:
rpow_natCast

Goal state after:
x y : ℝ
n : ℕ
hx : 0 ≤ x
h : y - ↑n ≠ 0
⊢ x ^ y / x ^ n = x ^ y / x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: y : ℝ
⊢ 0 ^ y = if y = 0 then 1 else 0

Tactic:
by
  split_ifs with h <;> simp [h]

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n : ℕ
z : ℝ
⊢ (x ^ ↑n) ^ z = (x ^ n) ^ z

Tactic:
rpow_natCast

Goal state after:
x : ℝ
hx : 0 ≤ x
n : ℕ
z : ℝ
⊢ (x ^ n) ^ z = (x ^ n) ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℕ
⊢ (x ^ y) ^ ↑n = (x ^ y) ^ n

Tactic:
rpow_natCast

Goal state after:
x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℕ
⊢ (x ^ y) ^ n = (x ^ y) ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: a b : ℂ
h : b ≠ 0
⊢ ContinuousAt (fun x ↦ a ^ x) b

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
a b : ℂ
h : b ≠ 0
ha : a = 0
⊢ ContinuousAt (fun x ↦ a ^ x) b

case neg
a b : ℂ
h : b ≠ 0
ha : ¬a = 0
⊢ ContinuousAt (fun x ↦ a ^ x) b
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
n : ℕ
z : ℝ
⊢ (x ^ ↑n) ^ z = (x ^ n) ^ z

Tactic:
rpow_natCast

Goal state after:
x : ℝ≥0
n : ℕ
z : ℝ
⊢ (x ^ n) ^ z = (x ^ n) ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0
y : ℝ
n : ℕ
⊢ (x ^ y) ^ ↑n = (x ^ y) ^ n

Tactic:
rpow_natCast

Goal state after:
x : ℝ≥0
y : ℝ
n : ℕ
⊢ (x ^ y) ^ n = (x ^ y) ^ n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx0 : 0 ≤ x
hx1 : x ≤ 1
hyz : z ≤ y
h : x = 0 → y = 0 → z = 0
⊢ x ^ y ≤ x ^ z

Tactic:
rcases eq_or_lt_of_le hx0 with (rfl | hx0')

Goal state after:
case inl
y z : ℝ
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
h : 0 = 0 → y = 0 → z = 0
⊢ 0 ^ y ≤ 0 ^ z

case inr
x y z : ℝ
hx0 : 0 ≤ x
hx1 : x ≤ 1
hyz : z ≤ y
h : x = 0 → y = 0 → z = 0
hx0' : 0 < x
⊢ x ^ y ≤ x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: case inr.inl
x : ℝ≥0∞
⊢ ContinuousAt (fun a ↦ a ^ 0) x

Tactic:
simp only [rpow_zero]

Goal state after:
case inr.inl
x : ℝ≥0∞
⊢ ContinuousAt (fun a ↦ 1) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
n : ℕ
hx : 0 < x
hy : 0 < y
⊢ x ^ n ≤ y ↔ x ^ ↑n ≤ y

Tactic:
rpow_natCast

Goal state after:
x y : ℝ
n : ℕ
hx : 0 < x
hy : 0 < y
⊢ x ^ n ≤ y ↔ x ^ n ≤ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
n : ℕ
hx : 0 < x
hy : 0 < y
⊢ x ^ n < y ↔ x ^ ↑n < y

Tactic:
rpow_natCast

Goal state after:
x y : ℝ
n : ℕ
hx : 0 < x
hy : 0 < y
⊢ x ^ n < y ↔ x ^ n < y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ ‖↑↑p ^ (-s)‖ ≤ 1 / 2

Tactic:
rw [norm_natCast_cpow_of_re_ne_zero p <| by rw [neg_re]; linarith only [hs]]
  refine (Real.rpow_le_rpow_of_nonpos zero_lt_two (Nat.cast_le.mpr p.prop.two_le) <|
    by rw [neg_re]; linarith only [hs]).trans ?_
  rw [one_div, ← Real.rpow_neg_one]
  exact Real.rpow_le_rpow_of_exponent_le one_le_two <| (neg_lt_neg hs).le

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

Goal state before:
pp: case pos.inl.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
Hz : z < 0
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos]

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

Goal state before:
pp: case pos.inl.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
Hz : z = 0
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos]

Goal state after:
case pos.inl.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
Hz : z = 0
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos.inl.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
Hz : 0 < z
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos]

Goal state after:
case pos.inl.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y < 0
Hz : 0 < z
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos.inr.inl.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y = 0
Hz : z < 0
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos]

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

Goal state before:
pp: case pos.inr.inl.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y = 0
Hz : z = 0
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos]

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

Goal state before:
pp: case pos.inr.inl.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y = 0
Hz : 0 < z
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos]

Goal state after:
case pos.inr.inl.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : y = 0
Hz : 0 < z
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos.inr.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : 0 < y
Hz : z < 0
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos]

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

Goal state before:
pp: case pos.inr.inr.inr.inl
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : 0 < y
Hz : z = 0
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos]

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

Goal state before:
pp: case pos.inr.inr.inr.inr
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : ↑x ≤ 1
h : x = 0
Hy : 0 < y
Hz : 0 < z
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
simp [Hy, Hz, h, zero_rpow_of_neg, zero_rpow_of_pos]

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
⊢ 0 < ↑n ^ ↑x

Tactic:
show (n : ℂ) ^ (x : ℂ) = (n : ℝ) ^ (x : ℂ) from rfl,

Goal state after:
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ 0 < ↑↑n ^ ↑x
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
n : ℕ
z : ℝ
⊢ (x ^ ↑n) ^ z = (x ^ n) ^ z

Tactic:
rpow_natCast

Goal state after:
x : ℝ≥0∞
n : ℕ
z : ℝ
⊢ (x ^ n) ^ z = (x ^ n) ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
y : ℝ
n : ℕ
⊢ (x ^ y) ^ ↑n = (x ^ y) ^ n

Tactic:
rpow_natCast

Goal state after:
x : ℝ≥0∞
y : ℝ
n : ℕ
⊢ (x ^ y) ^ n = (x ^ y) ^ n
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
p₁ p₂ : P
⊢ midpoint R p₁ p₂ -ᵥ p₂ = ⅟2 • (p₁ -ᵥ p₂)

Tactic:
by
  rw [midpoint_comm, midpoint_vsub_left]

Goal state after:
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 : E
s : Set E
hs : StarConvex 𝕜 x s
z y : E
hy : y ∈ (fun x ↦ z + x) '' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • (z + x) + b • y ∈ (fun x ↦ z + x) '' s

Tactic:
obtain ⟨y', hy', rfl⟩ := hy

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
⊢ a • (z + x) + b • (fun x ↦ z + x) y' ∈ (fun x ↦ z + x) '' s
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 : E
s : Set E
hs : StarConvex 𝕜 x s
z y : E
hy : y ∈ (fun x ↦ x + z) '' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • (x + z) + b • y ∈ (fun x ↦ x + z) '' s

Tactic:
obtain ⟨y', hy', rfl⟩ := hy

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
s : Set E
P : Prop
hs : Convex 𝕜 s
⊢ Convex 𝕜 {x | P → x ∈ s}

Tactic:
by_cases hP : P

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
s : Set E
P : Prop
hs : Convex 𝕜 s
hP : P
⊢ Convex 𝕜 {x | P → x ∈ s}

case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
s : Set E
P : Prop
hs : Convex 𝕜 s
hP : ¬P
⊢ Convex 𝕜 {x | P → x ∈ s}
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 : E
⊢ Convex 𝕜 ((fun x ↦ z + x) ⁻¹' s)

Tactic:
intro x hx y hy a b ha hb hab
  have h := hs hx hy ha hb hab
  rwa [smul_add, smul_add, add_add_add_comm, ← add_smul, hab, one_smul] at h

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ∃ z ∈ s, (p + q) • z = p • x + q • y

Tactic:
rcases _root_.em (p = 0 ∧ q = 0) with (⟨rfl, rfl⟩ | hpq)
  · use x, hx
    simp
  · replace hpq : 0 < p + q :=
      (add_nonneg hp hq).lt_of_ne' (mt (add_eq_zero_iff_of_nonneg hp hq).1 hpq)
    refine ⟨_, convex_iff_div.1 h hx hy hp hq hpq, ?_⟩
    match_scalars <;> field

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

Goal state before:
pp: case inl
𝕜 : 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
hxy : x ≤ y
⊢ [x -[𝕜] y] ⊆ s

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:
· exact (segment_subset_Icc hxy).trans (hs.out hx hy)

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
⊢ [x -[𝕜] y] ⊆ s
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ a • ⋃ r, ⋃ (_ : ‖r‖ ≤ 1), r • s ⊆ ⋃ r, ⋃ (_ : ‖r‖ ≤ 1), r • s

Tactic:
smul_set_iUnion₂,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ ⋃ i, ⋃ (_ : ‖i‖ ≤ 1), a • i • s ⊆ ⋃ r, ⋃ (_ : ‖r‖ ≤ 1), r • 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 ↦ id i.1 ×ˢ id i.2
⊢ Absorbs 𝕜 U s

Tactic:
simp_rw [← nhds_prod_eq, id] at h'

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
⊢ Absorbs 𝕜 U s
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: case inr.inr
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : AddCommMonoid β
inst✝² : PartialOrder β
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
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 : a + b = 1
ha' : 0 < a
hb' : 0 < b
⊢ f (a • x + b • y) ≤ a • f x + b • f y

Tactic:
exact h hx hy ha' hb' hab

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✝³ : Module 𝕜 E
inst✝² : Module 𝕜 β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : StrictConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ {x | x ∈ s ∧ f x < r}
y : E
hy : y ∈ {x | x ∈ s ∧ f x < r}
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • f x + b • f y ≤ a • r + b • r

Tactic:
by
          gcongr
          · exact hx.2.le
          · exact hy.2.le

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
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
| vectorSpan k (p '' s)

Tactic:
vectorSpan_eq_span_vsub_set_left k (Set.mem_image_of_mem p hi),

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
ι : Type u_4
p : ι → P
s : Set ι
i : ι
hi : i ∈ s
| Submodule.span k ((fun x ↦ p i -ᵥ x) '' p '' s)
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : SMul 𝕜 α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : StrictConcaveOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
hxy' : x' ≠ y'
⊢ a • f x' + b • f y' < f (a • x' + b • y')

Tactic:
exact hf.2 (by simp : x' ∈ univ) (by simp : y' ∈ univ) hxy' ha hb hab

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : SMul 𝕜 α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : SMul 𝕜 β
f : α ≃o β
hf : StrictConvexOn 𝕜 univ ⇑f
x : β
x✝¹ : x ∈ univ
y : β
x✝ : y ∈ univ
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : α
hx'' : x = f x'
y' : α
hy'' : y = f y'
hxy' : x' ≠ y'
⊢ f (a • x' + b • y') < a • f x' + b • f y'

Tactic:
exact hf.2 (by simp : x' ∈ univ) (by simp : y' ∈ univ) hxy' ha hb hab

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

Goal state before:
pp: ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : (Finsupp.linearCombination k fun i ↦ p i -ᵥ p i0) l = v
w : ι → k := ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hwdef : w = ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
⊢ ∑ i ∈ insert i0 l.support, l i -
      ∑ x ∈ insert i0 l.support, Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i) x =
    0

Tactic:
Finset.sum_update_of_mem (Finset.mem_insert_self _ _),

Goal state after:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
v : V
p : ι → P
i0 : ι
l : ι →₀ k
left✝ : l ∈ Finsupp.supported k k Set.univ
hv : (Finsupp.linearCombination k fun i ↦ p i -ᵥ p i0) l = v
w : ι → k := ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
hwdef : w = ⇑l - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)
⊢ ∑ i ∈ insert i0 l.support, l i - (∑ i ∈ l.support, l i + ∑ x ∈ insert i0 l.support \ {i0}, Function.const ι 0 x) = 0
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
x : E
r : ℝ
hr : r < 0
⊢ p.closedBall x r = ∅

Tactic:
by
  ext
  rw [Seminorm.mem_closedBall, Set.mem_empty_iff_false, iff_false, not_le]
  exact hr.trans_le (apply_nonneg _ _)

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inl
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
⊢ p.ball 0 (‖0‖ * r) ⊆ 0 • p.ball 0 r

Tactic:
rw [norm_zero, zero_mul, ball_eq_emptyset _ le_rfl]
    exact empty_subset _

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i j : ι
e✝ e : ι ≃ ι'
⊢ affineSpan k (range ⇑b) = ⊤

Tactic:
exact b.3

Goal state after: