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

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℂ
⊢ Tendsto f l (comap re atBot) ↔ Tendsto (fun x ↦ (f x).re) l atBot

Tactic:
tendsto_comap_iff

Goal state after:
α : Type u_1
l : Filter α
f : α → ℂ
⊢ Tendsto (re ∘ f) l atBot ↔ Tendsto (fun x ↦ (f x).re) l atBot
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c ↦ c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
⊢ 1 ∈ f ⁻¹' interior (closedBall x (dist y x))

Tactic:
by simpa [f]

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁵ : Field R
inst✝⁴ : Field S
inst✝³ : LinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : v a < 1
h_add : Tendsto (fun x ↦ 1 + v a ^ x) atTop (𝓝 (1 + 0))
h_sub : Tendsto (fun x ↦ 1 - v a ^ x) atTop (𝓝 (1 - 0))
⊢ Tendsto ?m.138 atTop (𝓝 1)

Tactic:
simpa using h_add

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

Goal state before:
pp: ⊢ √3 ^ 2 / 2 ^ 2 = 3 / 4

Tactic:
sq_sqrt

Goal state after:
⊢ 3 / 2 ^ 2 = 3 / 4

⊢ 0 ≤ 3
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p : ℝ
x : AddCircle p
hp : p ≠ 0
⊢ ‖x‖ ≤ |p| / 2

Tactic:
obtain ⟨x⟩ := x
  change ‖(x : AddCircle p)‖ ≤ |p| / 2
  rw [norm_eq, ← mul_le_mul_iff_right₀ (abs_pos.mpr (inv_ne_zero hp)), ← abs_mul, mul_sub,
    mul_left_comm, ← mul_div_assoc, ← abs_mul, inv_mul_cancel₀ hp, mul_one, abs_one]
  exact abs_sub_round (p⁻¹ * x)

Goal state after:
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr
p x : ℝ
hp✝ : p ≠ 0
hx : |x| ≤ |p| / 2
this : ∀ (p : ℝ), 0 < p → |x| ≤ p / 2 → ‖↑x‖ = |x|
hp : p < 0
⊢ ‖↑x‖ = |x|

Tactic:
· rw [← norm_neg_period]
      rw [abs_eq_neg_self.mpr hp.le] at hx
      exact this (-p) (neg_pos.mpr hp) hx

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

Goal state before:
pp: case pos
x : ℝ
h_zero : x = 0
⊢ 0 ≤ rexp 0

Tactic:
exp_zero

Goal state after:
case pos
x : ℝ
h_zero : x = 0
⊢ 0 ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: ⊢ 1 = rexp 0

Tactic:
exp_zero

Goal state after:
⊢ 1 = 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: ⊢ arg 1 = 0

Tactic:
simp [arg, zero_le_one]

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

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

Tactic:
by
  rw [log, norm_exp, Real.log_exp, arg_exp]

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

Goal state before:
pp: x : ℂ
hx_re : x.re < 0
hx_im : 0 ≤ x.im
⊢ x.arg = Real.arcsin ((-x).im / ‖x‖) + π

Tactic:
simp only [arg, hx_re.not_ge, hx_im, if_true, if_false]

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

Goal state before:
pp: case hx₁
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ 0 ≤ -z.arg

pp: case hx₂
z : ℂ
hz : z.im < 0
h₀ : z ≠ 0
⊢ -z.arg ≤ π

Tactic:
exacts [neg_nonneg.2 (arg_neg_iff.2 hz).le, neg_le.2 (neg_pi_lt_arg z).le]

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

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

Tactic:
refine mul_nonneg ?_ h1.le

Goal state after:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ -log x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
h : x.arg ≠ π
⊢ log ((starRingEnd ℂ) x) = (starRingEnd ℂ) (log x)

Tactic:
rw [log_conj_eq_ite, if_neg h]

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

Goal state before:
pp: case inr.inr
x : ℂ
hx : x ≠ 0
hi : 0 < x.im
⊢ ↑x.arg - ↑π = ↑x.arg + ↑π

Tactic:
Real.Angle.sub_coe_pi_eq_add_coe_pi

Goal state after:
case inr.inr
x : ℂ
hx : x ≠ 0
hi : 0 < x.im
⊢ ↑x.arg + ↑π = ↑x.arg + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case pos
x : ℂ
h : x ≠ 0
hs : x ∈ slitPlane
⊢ ContinuousAt (Real.Angle.coe ∘ arg) x

pp: case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt (Real.Angle.coe ∘ arg) x

Tactic:
· exact Real.Angle.continuous_coe.continuousAt.comp (continuousAt_arg hs)

Goal state after:
case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt (Real.Angle.coe ∘ arg) x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt (Real.Angle.coe ∘ arg) x

Tactic:
← Function.comp_id (((↑) : ℝ → Real.Angle) ∘ arg),

Goal state after:
case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt ((Real.Angle.coe ∘ arg) ∘ id) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 < x
y : ℝ
⊢ 0 < x ^ y

Tactic:
rw [rpow_def_of_pos hx]; apply exp_pos

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

Goal state before:
pp: ⊢ Tendsto (fun x ↦ x ^ (1 / x)) atTop (𝓝 1)

Tactic:
by
  convert! tendsto_rpow_div_mul_add (1 : ℝ) _ (0 : ℝ) zero_ne_one
  ring

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

Goal state before:
pp: w x y z : ℝ
hx : 0 ≤ x
hw : w ≠ 0
h : y + z = w
⊢ y + z ≠ 0

Tactic:
rwa [h]

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

Tactic:
rcases le_iff_eq_or_lt.1 hx with (H | pos)

Goal state after:
case inl
x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

case inr
x : ℝ
hx : 0 ≤ x
y z : ℝ
pos : 0 < x
⊢ x ^ y * x ^ z ≤ x ^ (y + z)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedRing E
a b c : ℝ
f g : ℝ → E
hf : f =O[atTop] fun t ↦ t ^ a
hg : g =O[atTop] fun t ↦ t ^ b
h : a + b ≤ c
⊢ (f * g) =O[atTop] fun t ↦ t ^ c

Tactic:
by
  refine (hf.mul hg).trans (Eventually.isBigO ?_)
  filter_upwards [eventually_ge_atTop 1] with t ht
  rw [← Real.rpow_add (zero_lt_one.trans_le ht), Real.norm_of_nonneg (Real.rpow_nonneg
    (zero_le_one.trans ht) (a + b))]
  exact Real.rpow_le_rpow_of_exponent_le ht h

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

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

Tactic:
by
  have cpow_eq : (fun x : ℂ => a ^ x) = fun x => exp (log a * x) := by
    ext1 b
    rw [cpow_def_of_ne_zero ha]
  rw [cpow_eq]
  exact continuous_exp.continuousAt.comp (ContinuousAt.mul continuousAt_const continuousAt_id)

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

Goal state before:
pp: case h
w y z : ℝ
x : ℝ≥0
hw : w ≠ 0
h : y + z = w
⊢ y + z ≠ 0

Tactic:
rwa [h]

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

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

Tactic:
rw [← ENNReal.some_eq_coe]
  dsimp only [(· ^ ·), Pow.pow, rpow]
  simp [h]

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

Goal state before:
pp: case inl
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
this : ContinuousAt (fun p ↦ (↑p.1, p.2)) (x, y)
⊢ ContinuousAt (fun p ↦ ↑p.1 ^ p.2) (x, y)

Tactic:
refine (continuousAt_cpow (Or.inl ?_)).comp this

Goal state after:
case inl
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
this : ContinuousAt (fun p ↦ (↑p.1, p.2)) (x, y)
⊢ 0 < (↑(x, y).1, (x, y).2).1.re
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < y ^ m
n : ℕ
hn : m + 1 ≤ n
⊢ x ^ (1 / ↑n) ≤ y

Tactic:
simp only [one_div]

Goal state after:
x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < y ^ m
n : ℕ
hn : m + 1 ≤ n
⊢ x ^ (↑n)⁻¹ ≤ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
lift x to ℝ≥0 using ne_of_lt (lt_of_le_of_lt hx coe_lt_top)
  simp only [coe_le_one_iff] at hx
  simp [← coe_rpow_of_nonneg _ hz, NNReal.rpow_le_one hx hz]

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

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

Tactic:
by
  refine RCLike.inv_pos_of_pos ?_
  rw [show (n : ℂ) ^ (x : ℂ) = (n : ℝ) ^ (x : ℂ) from rfl, ← ofReal_cpow n.cast_nonneg']
  positivity

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton M
x y : M
⊢ SameRay R x y

Tactic:
by
  rw [Subsingleton.elim x 0]
  exact zero_left _

Goal state after:
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 : P
⊢ midpoint R p₁ p₂ -ᵥ p = ⅟2 • (p₁ -ᵥ p₂) + (p₂ -ᵥ p)

Tactic:
← vadd_vsub_assoc,

Goal state after:
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 : P
⊢ midpoint R p₁ p₂ -ᵥ p = (⅟2 • (p₁ -ᵥ p₂) +ᵥ p₂) -ᵥ p
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
f g : P1 →ᵃ[k] P2
h : f = g
⊢ P1

Tactic:
inhabit P1

Goal state after:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
f g : P1 →ᵃ[k] P2
h : f = g
inhabited_h : Inhabited P1
⊢ P1
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_2.inl.inr.inr
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 : m 0 < 0
hm1 : 0 < m 1
⊢ SameRay R x y ∨ SameRay R x (-y)

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

Goal state after:
case neg.refine_2.inl.inr.inr
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 : m 0 < 0
hm1 : 0 < m 1
⊢ -m 0 • x = m 1 • y
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
inst✝¹ : IsDomain k
inst✝ : IsTorsionFree k V1
p₀ p₁ : P1
c₁ c₂ : k
⊢ c₁ • (p₁ -ᵥ p₀) - c₂ • (p₁ -ᵥ p₀) = 0 ↔ p₀ = p₁ ∨ c₁ = c₂

Tactic:
←
    sub_smul,

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
inst✝¹ : IsDomain k
inst✝ : IsTorsionFree k V1
p₀ p₁ : P1
c₁ c₂ : k
⊢ (c₁ - c₂) • (p₁ -ᵥ p₀) = 0 ↔ p₀ = p₁ ∨ c₁ = c₂
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_2.inr.inr.inr.inr
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 : 0 < m 1
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
· refine Or.inr (Or.inr (Or.inr ⟨m 0, m 1, hm0, hm1, ?_⟩))
      rwa [smul_neg]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
⊢ [x -[𝕜] y] = (fun θ ↦ x + θ • (y - x)) '' Icc 0 1

Tactic:
by
  convert! segment_eq_image 𝕜 x y using 2
  simp only [smul_sub, sub_smul, one_smul]
  abel

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
⊢ ↑s.direction = (fun x ↦ x -ᵥ p) '' ↑s

Tactic:
by
  rw [coe_direction_eq_vsub_set ⟨p, hp⟩]
  refine le_antisymm ?_ ?_
  · rintro v ⟨p₁, hp₁, p₂, hp₂, rfl⟩
    exact ⟨(p₁ -ᵥ p₂) +ᵥ p,
      vadd_mem_of_mem_direction (vsub_mem_direction hp₁ hp₂) hp, vadd_vsub _ _⟩
  · rintro v ⟨p₂, hp₂, rfl⟩
    exact ⟨p₂, hp₂, p, hp, rfl⟩

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
⊢ StarConvex 𝕜 x s ↔ s.OrdConnected

Tactic:
ordConnected_iff_uIcc_subset_left hx,

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
⊢ StarConvex 𝕜 x s ↔ ∀ ⦃y : 𝕜⦄, y ∈ s → uIcc x y ⊆ s
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : (x : P) → x ∈ affineSpan k s → Prop
mem : ∀ (y : P) (hys : y ∈ s), p y ⋯
smul_vsub_vadd :
  ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) ⋯
x : P
h : x ∈ affineSpan k s
⊢ ∃ (hx : x ∈ affineSpan k s), p x hx

Tactic:
refine affineSpan_induction h ?mem ?smul_vsub_vadd

Goal state after:
case mem
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 : (x : P) → x ∈ affineSpan k s → Prop
mem : ∀ (y : P) (hys : y ∈ s), p y ⋯
smul_vsub_vadd :
  ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) ⋯
x : P
h : x ∈ affineSpan k s
⊢ ∀ x ∈ s, ∃ (hx : x ∈ affineSpan k s), p x hx

case smul_vsub_vadd
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 : (x : P) → x ∈ affineSpan k s → Prop
mem : ∀ (y : P) (hys : y ∈ s), p y ⋯
smul_vsub_vadd :
  ∀ (c : k) (u : P) (hu : u ∈ affineSpan k s) (v : P) (hv : v ∈ affineSpan k s) (w : P) (hw : w ∈ affineSpan k s),
    p u hu → p v hv → p w hw → p (c • (u -ᵥ v) +ᵥ w) ⋯
x : P
h : x ∈ affineSpan k s
⊢ ∀ (c : k) (u v w : P),
    (∃ (hx : u ∈ affineSpan k s), p u hx) →
      (∃ (hx : v ∈ affineSpan k s), p v hx) →
        (∃ (hx : w ∈ affineSpan k s), p w hx) → ∃ (hx : c • (u -ᵥ v) +ᵥ w ∈ affineSpan k s), p (c • (u -ᵥ v) +ᵥ w) hx
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✝³ : TopologicalSpace E
inst✝² : T1Space E
inst✝¹ : RegularSpace E
inst✝ : ContinuousConstSMul 𝕜 E
a : Set E
ha : IsVonNBounded 𝕜 a
⊢ IsVonNBounded 𝕜 (closure[inst✝³] a)

Tactic:
intro V

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : T1Space E
inst✝¹ : RegularSpace E
inst✝ : ContinuousConstSMul 𝕜 E
a : Set E
ha : IsVonNBounded 𝕜 a
V : Set E
⊢ V ∈ 𝓝 0 → Absorbs 𝕜 V (closure[inst✝³] a)
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
⊢ IsVonNBounded 𝕜 s

Tactic:
intro V

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
⊢ V ∈ 𝓝 0 → Absorbs 𝕜 V s
Module: Mathlib.Analysis.Convex.Function

Goal state before:
pp: case refine_1
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
s : Set E
f g : E → β
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ a • (f ⊔ g) x + b • (f ⊔ g) y

Tactic:
calc
      f (a • x + b • y) ≤ a • f x + b • f y := hf.right hx hy ha hb hab
      _ ≤ a • (f x ⊔ g x) + b • (f y ⊔ g y) := by gcongr <;> apply le_sup_left

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid β
inst✝⁴ : LinearOrder β
inst✝³ : IsOrderedCancelAddMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulStrictMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hyz : f y ≤ f (a • x + b • y)
⊢ f (a • x + b • y) ≤ f x

Tactic:
exact hf.le_left_of_right_le' hx hy ha hb.le hab hyz

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 ι
w : ι → k
p₁ : ι → P
p₂ b : P
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂) = (s.weightedVSubOfPoint p₁ b) w - (∑ i ∈ s, w i) • (p₂ -ᵥ b)

Tactic:
rw [sum_smul_vsub_eq_weightedVSubOfPoint_sub, weightedVSubOfPoint_apply_const]

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 ι
w : ι → k
p₂ : ι → P
p₁ b : P
⊢ ∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) = (∑ i ∈ s, w i) • (p₁ -ᵥ b) - (s.weightedVSubOfPoint p₂ b) w

Tactic:
rw [sum_smul_vsub_eq_weightedVSubOfPoint_sub, weightedVSubOfPoint_apply_const]

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 : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ s
⊢ (affineSpan k (insert p₂ ↑s)).direction = k ∙ (p₂ -ᵥ p₁) ⊔ s.direction

Tactic:
rw [sup_comm, ← Set.union_singleton, ← coe_affineSpan_singleton k V p₂]

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 : AffineSubspace k P
p₁ p₂ : P
hp₁ : p₁ ∈ s
⊢ (affineSpan k (↑s ∪ ↑(affineSpan k {p₂}))).direction = s.direction ⊔ k ∙ (p₂ -ᵥ p₁)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case inl
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q✝ : Seminorm 𝕜 E
x✝ : E
p q : Seminorm 𝕜 E
x : E
⊢ ⨅ u, p u + q (0 • x - u) = ‖0‖ * ⨅ u, p u + q (x - u)

pp: case inr
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q✝ : Seminorm 𝕜 E
x✝ : E
p q : Seminorm 𝕜 E
a : 𝕜
x : E
ha : a ≠ 0
⊢ ⨅ u, p u + q (a • x - u) = ‖a‖ * ⨅ u, p u + q (x - u)

Tactic:
· rw [norm_zero, zero_mul, zero_smul]
          refine
            ciInf_eq_of_forall_ge_of_forall_gt_exists_lt
              (fun i => by positivity)
              fun x hx => ⟨0, by rwa [map_zero, sub_zero, map_zero, add_zero]⟩

Goal state after:
case inr
R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q✝ : Seminorm 𝕜 E
x✝ : E
p q : Seminorm 𝕜 E
a : 𝕜
x : E
ha : a ≠ 0
⊢ ⨅ u, p u + q (a • x - u) = ‖a‖ * ⨅ u, p u + q (x - u)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (DFunLike.coe '' s)
x : E
i : ↑s
⊢ ↑i (-x) = ↑i x

Tactic:
exact i.1.neg' _

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x ↦ Exists.choose ⋯
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x ↦ f ⟨↑x, ⋯⟩
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
x y : ↑ps
h : f' x = f' y
⊢ ↑x = ↑y

Tactic:
← (hf' x).2,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst✝ : Fintype ↑ps
hps : ps = p '' ↑s
f : ↑(p '' ↑s) → ι := fun x ↦ Exists.choose ⋯
hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x
f' : ↑ps → ι := fun x ↦ f ⟨↑x, ⋯⟩
hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x
x y : ↑ps
h : f' x = f' y
⊢ p (f' x) = ↑y
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, w i = 0

Tactic:
hwdef

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 - Function.update (Function.const ι 0) i0 (∑ i ∈ l.support, l i)) i = 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
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.ball 0 r
hx : (fun x ↦ a • x) y = x
⊢ ‖a‖ * p y < r

Tactic:
calc
    _ ≤ p y := mul_le_of_le_one_left (apply_nonneg p _) ha
    _ < r := by rwa [mem_ball_zero] at hy

Goal state after: