mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ ↑(sinOrderIso.symm (projIcc (-1) 1 ⋯ x)) = ↑((⇑sinOrderIso.symm ∘ projIcc (-1) 1 arcsin._proof_2) x)

Tactic:
Function.comp_apply

Goal state after:
x : ℝ
⊢ ↑(sinOrderIso.symm (projIcc (-1) 1 ⋯ x)) = ↑(sinOrderIso.symm (projIcc (-1) 1 arcsin._proof_2 x))
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ < -(π / 2) ∨ π / 2 < θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Tactic:
rcases h₁ with h₁ | h₁

Goal state after:
case neg.inl
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ < -(π / 2)
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

case neg.inr
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : π / 2 < θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.inl
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ < -(π / 2)
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Tactic:
replace hθ := hθ.1

Goal state after:
case neg.inl
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
⊢ x ≤ rexp (log x)

Tactic:
by_cases h_zero : x = 0
  · rw [h_zero, log, dif_pos rfl, exp_zero]
    exact zero_le_one
  · rw [exp_log_eq_abs h_zero]
    exact le_abs_self _

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

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

Tactic:
convert! toIocMod_mem_Ioc ..
    ring

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

Goal state before:
pp: θ : ℝ
⊢ (cexp (↑θ * I)).arg = toIocMod Real.two_pi_pos (-π) θ

Tactic:
by
  simp [arg_exp]

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

Goal state before:
pp: case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + N • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
⊢ z.arg ∈ Ioc (-π) π

Tactic:
two_mul,

Goal state after:
case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + N • (π + π) ∈ Ioc (-π) (-π + (π + π))
⊢ z.arg ∈ Ioc (-π) π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x.arg = y.arg ↔ (↑‖y‖ / ↑‖x‖ * x).arg = y.arg

Tactic:
rw [← ofReal_div, arg_real_mul]

Goal state after:
case hr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ 0 < ‖y‖ / ‖x‖
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: n : ℕ
⊢ 0 ≤ log (-↑n)

Tactic:
by
  rw [← log_neg_eq_log, neg_neg]
  exact log_natCast_nonneg _

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

Goal state before:
pp: x : ℂ
⊢ ↑x.re + ↑(toIocMod Real.two_pi_pos (-π) x.im) * I = x - ↑(toIocDiv Real.two_pi_pos (-π) x.im) * (2 * ↑π * I)

Tactic:
toIocMod,

Goal state after:
x : ℂ
⊢ ↑x.re + ↑(x.im - toIocDiv Real.two_pi_pos (-π) x.im • (2 * π)) * I =
    x - ↑(toIocDiv Real.two_pi_pos (-π) x.im) * (2 * ↑π * I)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x y : ℂ
⊢ ¬x ^ y = 0 ↔ x ≠ 0 ∨ y = 0

Tactic:
cpow_eq_zero_iff,

Goal state after:
x y : ℂ
⊢ ¬(x = 0 ∧ y ≠ 0) ↔ x ≠ 0 ∨ y = 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (↑n / ↑d < -1) = true
⊢ 0 < Real.log (↑n / ↑d)

Tactic:
have : (n : ℝ) / d < -1 := by exact_mod_cast of_decide_eq_true h

Goal state after:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (↑n / ↑d < -1) = true
this : ↑n / ↑d < -1
⊢ 0 < Real.log (↑n / ↑d)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
| (↑θ.toReal).sin

Tactic:
sin_coe

Goal state after:
θ : Angle
| Real.sin θ.toReal
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case e'_5
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ 𝓝 (-π) = 𝓝 ((Real.arcsin ∘ (im ∘ Neg.neg / fun a ↦ ‖a‖)) z - π)

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

Tactic:
· simp [him]

Goal state after:
case convert_3
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ‖z‖ ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x ≤ 0
y : ℝ
⊢ x ^ y = if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y) * cos (y * π)

Tactic:
by
  split_ifs with h <;> simp [rpow_def, *]; exact rpow_def_of_neg (lt_of_le_of_ne hx h) _

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 : 0 ≤ f i ∧ ∀ x ∈ s, 0 ≤ f x
⊢ a ^ ∑ x ∈ cons i s hi, f x = ∏ x ∈ cons i s hi, a ^ f x

Tactic:
sum_cons,

Goal state after:
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 : 0 ≤ f i ∧ ∀ x ∈ s, 0 ≤ f x
⊢ a ^ (f i + ∑ x ∈ s, f x) = ∏ x ∈ cons i s hi, a ^ f x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
y : ℝ
⊢ (x ^ ↑y).re = ‖x‖ ^ y * Real.cos (x.arg * y)

Tactic:
by
  rw [cpow_ofReal]; generalize arg x * y = z; simp [Real.cos]

Goal state after:
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
  · rw [ha, continuousAt_congr (zero_cpow_eq_nhds h)]
    exact continuousAt_const
  · exact continuousAt_const_cpow ha

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

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

Tactic:
nth_rw 2 [← NNReal.rpow_one x]

Goal state after:
case inr
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
h : 0 < x
⊢ x ^ z ≤ x ^ 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inl.inl
z : ℝ
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
hyz : z ≤ 0
h : 0 = 0 → 0 = 0 → z = 0
⊢ 0 ^ 0 ≤ 0 ^ z

Tactic:
rw [h rfl rfl]

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

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

pp: 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

Tactic:
· rcases eq_or_ne y 0 with rfl | hy0
    · rw [h rfl rfl]
    · rw [zero_rpow hy0]
      apply zero_rpow_nonneg

Goal state after:
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.Real

Goal state before:
pp: case inr
x y p : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hp : 0 ≤ p
hxy : y ≤ x
⊢ x ^ p = max (x ^ p) (y ^ p)

Tactic:
max_eq_left (by gcongr)

Goal state after:
case inr
x y p : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hp : 0 ≤ p
hxy : y ≤ x
⊢ x ^ p = x ^ p
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: x : ℝ≥0∞
hx : x ≠ ∞
y : ℝ≥0∞
hy : 1 < y
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y

Tactic:
lift x to ℝ≥0 using hx

Goal state after:
y : ℝ≥0∞
hy : 1 < y
x : ℝ≥0
⊢ ∀ᶠ (n : ℕ) in atTop, ↑x ^ (1 / ↑n) ≤ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x ≠ 0
y : ℝ
hy : y ∈ {y | 0 ≤ y}
z : ℝ
hz : z ∈ {y | 0 ≤ y}
hyz : y ^ x = z ^ x
⊢ y = z

Tactic:
rw [← rpow_one y, ← rpow_one z, ← mul_inv_cancel₀ hx, rpow_mul hy, rpow_mul hz, hyz]

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

Goal state before:
pp: case neg
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : ¬x = ∞
⊢ ContinuousAt (fun a ↦ a ^ y) x

Tactic:
lift x to ℝ≥0 using hx

Goal state after:
case neg
y : ℝ
h : 0 < y
x : ℝ≥0
⊢ ContinuousAt (fun a ↦ a ^ y) ↑x
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr.inr
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
ry rz₂ : R
hry : 0 < ry
hrz₂ : 0 < rz₂
Hy : ry • y = rz₂ • z
⊢ SameRay R (x + y) z

Tactic:
refine Or.inr (Or.inr ⟨rx * ry, ry * rz₁ + rx * rz₂, mul_pos hrx hry, ?_, ?_⟩)

Goal state after:
case inr.inr.inr.refine_1
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
ry rz₂ : R
hry : 0 < ry
hrz₂ : 0 < rz₂
Hy : ry • y = rz₂ • z
⊢ 0 < ry * rz₁ + rx * rz₂

case inr.inr.inr.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
ry rz₂ : R
hry : 0 < ry
hrz₂ : 0 < rz₂
Hy : ry • y = rz₂ • z
⊢ (rx * ry) • (x + y) = (ry * rz₁ + rx * rz₂) • z
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
u : Rˣ
hu : 0 < ↑u
v✝ : M
hv✝ : v✝ ≠ 0
⊢ u • rayOfNeZero R v✝ hv✝ = rayOfNeZero R v✝ hv✝

Tactic:
smul_rayOfNeZero,

Goal state after:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
u : Rˣ
hu : 0 < ↑u
v✝ : M
hv✝ : v✝ ≠ 0
⊢ rayOfNeZero R (u • v✝) ⋯ = rayOfNeZero R v✝ hv✝
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

pp: case neg.refine_2
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 : ∃ g, ∑ i, g i • ![x, y] i = 0 ∧ ∃ i, g i ≠ 0
⊢ SameRay R x y ∨ SameRay R x (-y)

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:
case neg.refine_2
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 : ∃ g, ∑ i, g i • ![x, y] i = 0 ∧ ∃ i, g i ≠ 0
⊢ SameRay R x y ∨ SameRay R x (-y)
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_2.inr.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
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : m 1 < 0
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
refine Or.inl (Or.inr (Or.inr ⟨m 0, -m 1, hm0, Left.neg_pos_iff.2 hm1, ?_⟩))
      rwa [neg_smul]

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

Goal state before:
pp: case h₂
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst✝⁷ : Ring k
inst✝⁶ : AddCommGroup V2
inst✝⁵ : AffineSpace V2 P2
inst✝⁴ : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst✝³ : (i : ι) → AddCommGroup (φv i)
inst✝² : (i : ι) → Module k (φv i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)
h₂ : f 0 = g 0
⊢ f ?p✝ = g ?p✝

pp: case p
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst✝⁷ : Ring k
inst✝⁶ : AddCommGroup V2
inst✝⁵ : AffineSpace V2 P2
inst✝⁴ : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst✝³ : (i : ι) → AddCommGroup (φv i)
inst✝² : (i : ι) → Module k (φv i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)
h₂ : f 0 = g 0
⊢ (i : ι) → φv i

Tactic:
· exact h₂

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

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

Tactic:
simp only [add_sub_add_left_eq_sub]

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

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
⊢ (lineMap x y) a ∈
    insert ((lineMap x y) c) (⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1)

Tactic:
right
    left
    have hc : 0 < c := h₀.trans hac
    refine ⟨a / c, ⟨div_pos h₀ hc, (div_lt_one hc).2 hac⟩, ?_⟩
    simp only [← homothety_eq_lineMap, ← homothety_mul_apply, div_mul_cancel₀ _ hc.ne']

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

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hac : a < c
⊢ (lineMap x y) a ∈
    insert ((lineMap x y) c) (⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1)

pp: case inr.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
a : 𝕜
h₀ : 0 < a
h₁ : a < 1
⊢ (lineMap x y) a ∈
    insert ((lineMap x y) a) (⇑(lineMap x ((lineMap x y) a)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) a) y) '' Ioo 0 1)

pp: case inr.inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
⊢ (lineMap x y) a ∈
    insert ((lineMap x y) c) (⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1)

Tactic:
· right
    left
    have hc : 0 < c := h₀.trans hac
    refine ⟨a / c, ⟨div_pos h₀ hc, (div_lt_one hc).2 hac⟩, ?_⟩
    simp only [← homothety_eq_lineMap, ← homothety_mul_apply, div_mul_cancel₀ _ hc.ne']

Goal state after:
case inr.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
a : 𝕜
h₀ : 0 < a
h₁ : a < 1
⊢ (lineMap x y) a ∈
    insert ((lineMap x y) a) (⇑(lineMap x ((lineMap x y) a)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) a) y) '' Ioo 0 1)

case inr.inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
c a : 𝕜
h₀ : 0 < a
h₁ : a < 1
hca : c < a
⊢ (lineMap x y) a ∈
    insert ((lineMap x y) c) (⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1)
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : PosSMulMono 𝕜 E
x y : E
h : y ≤ x
⊢ [x -[𝕜] y] ⊆ Icc y x

Tactic:
segment_symm

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : PosSMulMono 𝕜 E
x y : E
h : y ≤ x
⊢ [y -[𝕜] x] ⊆ Icc y x
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 F
hs : StarConvex 𝕜 (f x) s
⊢ StarConvex 𝕜 x (⇑f ⁻¹' s)

Tactic:
by
  intro y hy a b ha hb hab
  rw [mem_preimage, Convex.combo_affine_apply hab]
  exact hs hy ha hb hab

Goal state after:
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:
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.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Balanced 𝕜 s
hs_nonempty : s.Nonempty
⊢ 0 ∈ s

Tactic:
← hs.balancedCore_eq

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Balanced 𝕜 s
hs_nonempty : (balancedCore 𝕜 s).Nonempty
⊢ 0 ∈ s
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ ((1 - a) / 2) • -x + ((a - -1) / 2) • x ∈ s

Tactic:
exact hs (h hx) hx (div_nonneg (sub_nonneg_of_le ha.2) zero_le_two)
    (div_nonneg (sub_nonneg_of_le ha.1) zero_le_two) (by ring)

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

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
⊢ ↑(affineSpan k (insert 0 s)) = ↑(Submodule.span k s)

Tactic:
rw [← Submodule.span_insert_zero]

Goal state after:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Set V
⊢ ↑(affineSpan k (insert 0 s)) = ↑(Submodule.span k (insert 0 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 : TotallyBounded s
h : ∃ x, 1 < ‖x‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁵, non_trivial := h }
⊢ Bornology.IsVonNBounded 𝕜 s

Tactic:
rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero] at hs

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 }
⊢ Bornology.IsVonNBounded 𝕜 s
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z x : E
hx : x ∈ (fun x ↦ z + x) ⁻¹' s
y : E
hy : y ∈ (fun x ↦ z + x) ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h : a • z + b • z + (a • x + b • y) ∈ interior s
⊢ a • x + b • y ∈ (fun x ↦ z + x) ⁻¹' interior s

Tactic:
← _root_.add_smul,

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z x : E
hx : x ∈ (fun x ↦ z + x) ⁻¹' s
y : E
hy : y ∈ (fun x ↦ z + x) ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h : (a + b) • z + (a • x + b • y) ∈ interior s
⊢ a • x + b • y ∈ (fun x ↦ z + x) ⁻¹' interior s
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✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hfg : EqOn f g s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ g (a • x + b • y) ≤ a • g x + b • g y

Tactic:
simpa only [← hfg hx, ← hfg hy, ← hfg (hf.1 hx hy ha hb hab)] using hf.2 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✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f g : E → β
hf : ConcaveOn 𝕜 s f
hfg : EqOn f g s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • g x + b • g y ≤ g (a • x + b • y)

Tactic:
simpa only [← hfg hx, ← hfg hy, ← hfg (hf.1 hx hy ha hb hab)] using hf.2 hx hy ha hb hab

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
s : Set P
p : P
hp : p ∈ s
| Submodule.span k ((fun x ↦ p -ᵥ x) '' s)

Tactic:
← Set.insert_eq_of_mem hp,

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
p : P
hp : p ∈ s
| Submodule.span k ((fun x ↦ p -ᵥ x) '' insert p s)
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
s : Set P
p : P
hp : p ∈ s
| Submodule.span k ((fun x ↦ x -ᵥ p) '' s)

Tactic:
← Set.insert_eq_of_mem hp,

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
p : P
hp : p ∈ s
| Submodule.span k ((fun x ↦ x -ᵥ p) '' insert p s)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
i : ι
hi : i ∈ s
⊢ p i ≤ ∑ x ∈ s \ {i}, p x + p i

Tactic:
le_add_iff_nonneg_left

Goal state after:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
i : ι
hi : i ∈ s
⊢ 0 ≤ ∑ x ∈ s \ {i}, p x