mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
har1 : |r| < 1
m : ℕ
hmn : n.succ ≤ m
hr : 0 < r
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m

Tactic:
generalize hk : m - n.succ = k

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
har1 : |r| < 1
m : ℕ
hmn : n.succ ≤ m
hr : 0 < r
k : ℕ
hk : m - n.succ = k
⊢ abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: ⊢ Set.range Subtype.val = Set.Ioi 0

Tactic:
Subtype.range_coe

Goal state after:
⊢ Set.Ioi 0 = Set.Ioi 0
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: k : ℕ
r : ℝ
hr : 0 < r
⊢ Summable fun n ↦ ↑n ^ k * rexp (-r * ↑n)

Tactic:
mul_comm (-r),

Goal state after:
k : ℕ
r : ℝ
hr : 0 < r
⊢ Summable fun n ↦ ↑n ^ k * rexp (↑n * -r)
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ x • ball 1 δ = ball x δ

Tactic:
rw [smul_ball, smul_eq_mul, mul_one]

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

Goal state before:
pp: n : ℕ
⊢ 1 - 2 / 2 ^ 2 - sqrtTwoAddSeries 0 n / 2 ^ 2 = 1 / 2 - sqrtTwoAddSeries 0 n / 4

Tactic:
congr
    · norm_num
    · norm_num

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ sphere x r \ ∅ = sphere x r

Tactic:
sdiff_empty

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ sphere x r = sphere x r
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ sphere x r \ ∅ = sphere x r

Tactic:
sdiff_empty

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ sphere x r = sphere x r
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set 𝕜
hs : 0 ∉ s
r : ℝ
c : 𝕜
hc : c ∈ s
⊢ c • sphere 0 r = sphere 0 (‖c‖ * r)

Tactic:
by
      rw [smul_sphere' (ne_of_mem_of_not_mem hc hs), smul_zero]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
h : dist x z < ε + δ
⊢ ε / (ε + δ) + δ / (ε + δ) = 1

Tactic:
rw [← add_div, div_self (add_pos_of_pos_of_nonneg hε hδ).ne']

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y x' y' : X
hx : x' = x
hy : y' = y
⊢ Bijective fun x_1 ↦ x_1.cast hx hy

Tactic:
subst_vars; exact bijective_id

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

Goal state before:
pp: case hbc
α : Type u_1
inst✝¹ : NormedDivisionRing α
inst✝ : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq fun n ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n‖ ≤ C / ‖w‖ ^ n
n : ℕ
⊢ ‖f n‖ ≤ C / ‖w‖ ^ n

Tactic:
exact hC n

Goal state after:
Module: Mathlib.Topology.Path

Goal state before:
pp: case refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ₂
h₁' : Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ₁ t).extend
h₂' : Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ₂ t).extend
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ (γ₂ p.1).extend (2 * ↑p.2 - 1)

pp: case refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ₂
h₁' : Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ₁ t).extend
h₂' : Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ₂ t).extend
⊢ ∀ (x : ι × ↑I), ↑x.2 = 1 / 2 → (γ₁ x.1).extend (2 * ↑x.2) = (γ₂ x.1).extend (2 * ↑x.2 - 1)

Tactic:
· change
      Continuous ((fun p : ι × ℝ => (γ₂ p.1).extend p.2) ∘ Prod.map id (fun x => 2 * x - 1 : I → ℝ))
    exact h₂'.comp (by fun_prop)

Goal state after:
case refine_3
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ₂
h₁' : Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ₁ t).extend
h₂' : Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ₂ t).extend
⊢ ∀ (x : ι × ↑I), ↑x.2 = 1 / 2 → (γ₁ x.1).extend (2 * ↑x.2) = (γ₂ x.1).extend (2 * ↑x.2 - 1)
Module: Mathlib.Analysis.Normed.Group.AddCircle

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

Tactic:
rw [abs_eq_self.mpr hp.le] at hx

Goal state after:
case inl
p x : ℝ
hp✝ : p ≠ 0
hx : |x| ≤ p / 2
this : ∀ (p : ℝ), 0 < p → |x| ≤ p / 2 → ‖↑x‖ = |x|
hp : 0 < p
⊢ ‖↑x‖ = |x|
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
this : round (p⁻¹ * x) = 0
⊢ ‖↑x‖ = |x|

Tactic:
by simp [norm_eq, this]

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

Goal state before:
pp: p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
m : ℕ
hm : ↑(↑m / ↑(addOrderOf u) * p) = u
⊢ ‖u‖ = p * (↑(min (m % n) (n - m % n)) / ↑n)

Tactic:
rw [← hm, norm_div_natCast]

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

Goal state before:
pp: case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
rw [not_le] at hx₁
    rw [arccos_of_le_neg_one hx₁.le, sin_pi, sqrt_eq_zero_of_nonpos]
    nlinarith

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

Goal state before:
pp: x : ℝ
⊢ 2 * x ≤ rexp x

Tactic:
by_cases hx0 : x < 0

Goal state after:
case pos
x : ℝ
hx0 : x < 0
⊢ 2 * x ≤ rexp x

case neg
x : ℝ
hx0 : ¬x < 0
⊢ 2 * x ≤ rexp x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ (rexp (log x) - rexp (-log x)) / 2 = (x - x⁻¹) / 2

Tactic:
exp_neg,

Goal state after:
x : ℝ
hx : 0 < x
⊢ (rexp (log x) - (rexp (log x))⁻¹) / 2 = (x - x⁻¹) / 2
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ (rexp (log x) + rexp (-log x)) / 2 = (x + x⁻¹) / 2

Tactic:
exp_neg,

Goal state after:
x : ℝ
hx : 0 < x
⊢ (rexp (log x) + (rexp (log x))⁻¹) / 2 = (x + x⁻¹) / 2
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case neg
x : ℝ
hx : ¬x = 0
⊢ |x⁻¹| = rexp (-log x)

Tactic:
exp_neg,

Goal state after:
case neg
x : ℝ
hx : ¬x = 0
⊢ |x⁻¹| = (rexp (log x))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case ofNat
x : ℝ
a✝ : ℕ
⊢ log (x ^ Int.ofNat a✝) = ↑(Int.ofNat a✝) * log x

Tactic:
rw [Int.ofNat_eq_natCast, zpow_natCast, log_pow, Int.cast_natCast]

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

Goal state before:
pp: case mpr
θ ψ : ℝ
⊢ (∃ k, θ - ψ = 2 * π * ↑k) ∨ ↑θ + ↑ψ = ↑π → sin θ = sin ψ

Tactic:
← eq_sub_iff_add_eq,

Goal state after:
case mpr
θ ψ : ℝ
⊢ (∃ k, θ - ψ = 2 * π * ↑k) ∨ ↑θ = ↑π - ↑ψ → sin θ = sin ψ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

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

Tactic:
half_sub,

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

Goal state before:
pp: x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0
    else if x.arg = π then cexp (-((starRingEnd ℂ) (log x) * n)) else cexp (-(log x * n))) =
    if x.arg = π then
      if x = 0 then if n = 0 then 1⁻¹ else 0⁻¹ else ((starRingEnd ℂ) (cexp (log x * (starRingEnd ℂ) n)))⁻¹
    else if x = 0 then if n = 0 then 1⁻¹ else 0⁻¹ else (cexp (log x * n))⁻¹

Tactic:
exp_neg,

Goal state after:
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0
    else if x.arg = π then (cexp ((starRingEnd ℂ) (log x) * n))⁻¹ else (cexp (log x * n))⁻¹) =
    if x.arg = π then
      if x = 0 then if n = 0 then 1⁻¹ else 0⁻¹ else ((starRingEnd ℂ) (cexp (log x * (starRingEnd ℂ) n)))⁻¹
    else if x = 0 then if n = 0 then 1⁻¹ else 0⁻¹ else (cexp (log x * n))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h
x✝ : ℝ
⊢ (↑x✝ + ↑π).cos = -(↑x✝).cos

Tactic:
exact Real.cos_antiperiodic _

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

Goal state before:
pp: θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ |θ.cos| = |ψ.sin|

Tactic:
← eq_sub_iff_add_eq,

Goal state after:
θ ψ : Angle
h : 2 • θ = ↑π - 2 • ψ
⊢ |θ.cos| = |ψ.sin|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

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

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

Goal state before:
pp: case mp.inr
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
h2 : a = b + ↑π
⊢ a = b

Tactic:
· have : a.sign = (b + π).sign := by aesop
      rw [Real.Angle.sign_add_pi] at this
      have := congr_arg (· = b.sign) this
      aesop

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

Goal state before:
pp: hb₀ : -1 < 0
hb₁ : 0 < 1
⊢ Tendsto (fun x ↦ 0 ^ x) atTop (𝓝 0)

Tactic:
refine Tendsto.mono_right ?_ (Iff.mpr pure_le_nhds_iff rfl)
    rw [tendsto_pure]
    filter_upwards [eventually_ne_atTop 0] with _ hx
    simp [hx]

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

Goal state before:
pp: case inl
y z : ℝ
h : y + z ≠ 0
hx : 0 ≤ 0
⊢ 0 ^ (y + z) = 0 ^ y * 0 ^ z

Tactic:
zero_rpow h,

Goal state after:
case inl
y z : ℝ
h : y + z ≠ 0
hx : 0 ≤ 0
⊢ 0 = 0 ^ y * 0 ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℂ
a b : ℂ
hf : Tendsto f l (𝓝 b)
h : a ≠ 0 ∨ b ≠ 0
⊢ Tendsto (fun x ↦ a ^ f x) l (𝓝 (a ^ b))

Tactic:
by
  cases h with
  | inl h => exact (continuousAt_const_cpow h).tendsto.comp hf
  | inr h => exact (continuousAt_const_cpow' h).tendsto.comp hf

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

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

Tactic:
have A : Tendsto (fun p : ℝ × ℝ => exp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0) :=
    tendsto_exp_atBot.comp
      ((tendsto_log_nhdsNE_zero.comp tendsto_fst).atBot_mul_pos hp tendsto_snd)

Goal state after:
case inr
y : ℝ
hp : 0 < y
A : Tendsto (fun p ↦ rexp (log p.1 * p.2)) (𝓝[≠] 0 ×ˢ 𝓝 y) (𝓝 0)
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) (0, 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:
← rpow_one y,

Goal state after:
x : ℝ
hx : x ≠ 0
y : ℝ
hy : y ∈ {y | 0 ≤ y}
z : ℝ
hz : z ∈ {y | 0 ≤ y}
hyz : y ^ x = z ^ x
⊢ y ^ 1 = z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case inr.inr
x y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hxy : x ≤ y
hx0 : x ≠ 0
hy0 : y ≠ 0
⊢ (x * y) ^ z = if (x = 0 ∧ y = ∞ ∨ x = ∞ ∧ y = 0) ∧ z < 0 then ∞ else x ^ z * y ^ z

Tactic:
induction x

Goal state after:
case inr.inr.top
y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hy0 : y ≠ 0
hxy : ∞ ≤ y
hx0 : ∞ ≠ 0
⊢ (∞ * y) ^ z = if (∞ = 0 ∧ y = ∞ ∨ ∞ = ∞ ∧ y = 0) ∧ z < 0 then ∞ else ∞ ^ z * y ^ z

case inr.inr.coe
y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hy0 : y ≠ 0
x✝ : ℝ≥0
hxy : ↑x✝ ≤ y
hx0 : ↑x✝ ≠ 0
⊢ (↑x✝ * y) ^ z = if (↑x✝ = 0 ∧ y = ∞ ∨ ↑x✝ = ∞ ∧ y = 0) ∧ z < 0 then ∞ else ↑x✝ ^ z * y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
⊢ √((‖x‖ + ‖x‖ * Real.cos x.arg) / 2) = √((‖x‖ + x.re) / 2)

pp: case hx
x : ℂ
⊢ 0 ≤ ‖x‖

pp: case hl
x : ℂ
⊢ -π ≤ x.arg

pp: case hr
x : ℂ
⊢ x.arg ≤ π

Tactic:
norm_mul_cos_arg

Goal state after:
x : ℂ
⊢ √((‖x‖ + x.re) / 2) = √((‖x‖ + x.re) / 2)

case hx
x : ℂ
⊢ 0 ≤ ‖x‖

case hl
x : ℂ
⊢ -π ≤ x.arg

case hr
x : ℂ
⊢ x.arg ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
hx : 0 ≤ x.im
⊢ √((‖x‖ - ‖x‖ * Real.cos x.arg) / 2) = √((‖x‖ - x.re) / 2)

pp: case hl
x : ℂ
hx : 0 ≤ x.im
⊢ 0 ≤ x.arg

pp: case hr
x : ℂ
hx : 0 ≤ x.im
⊢ x.arg ≤ 2 * π

Tactic:
norm_mul_cos_arg

Goal state after:
x : ℂ
hx : 0 ≤ x.im
⊢ √((‖x‖ - x.re) / 2) = √((‖x‖ - x.re) / 2)

case hl
x : ℂ
hx : 0 ≤ x.im
⊢ 0 ≤ x.arg

case hr
x : ℂ
hx : 0 ≤ x.im
⊢ x.arg ≤ 2 * π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
hx : x.im < 0
⊢ -√((‖x‖ - ‖x‖ * Real.cos x.arg) / 2) = -√((‖x‖ - x.re) / 2)

pp: case hl
x : ℂ
hx : x.im < 0
⊢ -(2 * π) ≤ x.arg

pp: case hr
x : ℂ
hx : x.im < 0
⊢ x.arg ≤ 0

Tactic:
norm_mul_cos_arg

Goal state after:
x : ℂ
hx : x.im < 0
⊢ -√((‖x‖ - x.re) / 2) = -√((‖x‖ - x.re) / 2)

case hl
x : ℂ
hx : x.im < 0
⊢ -(2 * π) ≤ x.arg

case hr
x : ℂ
hx : x.im < 0
⊢ x.arg ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
⊢ √((‖x‖ - ‖x‖ * Real.cos x.arg) / 2) = √((‖x‖ - x.re) / 2)

Tactic:
norm_mul_cos_arg

Goal state after:
x : ℂ
⊢ √((‖x‖ - x.re) / 2) = √((‖x‖ - x.re) / 2)
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
i : ι
x : φv i
s₁ : f (Pi.single i x) = g (Pi.single i x)
s₂ : f (Pi.single i x +ᵥ 0) = f.linear (Pi.single i x) +ᵥ f 0
⊢ f.linear (Pi.single i x) = g.linear (Pi.single i x)

Tactic:
have s₃ := g.map_vadd 0 (Pi.single i x)

Goal state after:
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
i : ι
x : φv i
s₁ : f (Pi.single i x) = g (Pi.single i x)
s₂ : f (Pi.single i x +ᵥ 0) = f.linear (Pi.single i x) +ᵥ f 0
s₃ : g (Pi.single i x +ᵥ 0) = g.linear (Pi.single i x) +ᵥ g 0
⊢ f.linear (Pi.single i x) = g.linear (Pi.single i x)
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 : P
v : V
hp : p ∈ spanPoints k s
hv : v ∈ vectorSpan k s
⊢ v +ᵥ p ∈ spanPoints k s

Tactic:
by
  rcases hp with ⟨p₂, ⟨hp₂, ⟨v₂, ⟨hv₂, hv₂p⟩⟩⟩⟩
  rw [hv₂p, vadd_vadd]
  exact ⟨p₂, hp₂, v + v₂, (vectorSpan k s).add_mem hv hv₂, rfl⟩

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
⊢ Convex 𝕜 (⇑f '' s)

Tactic:
by
  rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ a b ha hb hab
  exact ⟨a • x + b • y, hs hx hy ha hb hab, by rw [f.map_add, f.map_smul, f.map_smul]⟩

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : Ring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : IsStrictOrderedModule 𝕜 E
inst✝ : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
⊢ StarConvex 𝕜 y (Iic x)ᶜ

Tactic:
refine (starConvex_iff_forall_pos <| by simp [h.not_ge]).mpr fun z hz a b ha hb hab ↦ ?_
  rw [mem_compl_iff, mem_Iic] at hz ⊢
  contrapose hz
  refine (lt_of_smul_lt_smul_of_nonneg_left ?_ hb.le).le
  calc
    b • z ≤ (a + b) • x - a • y := by rwa [le_sub_iff_add_le', hab, one_smul]
    _ < b • x := by
      rw [add_smul, sub_lt_iff_lt_add']
      gcongr

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
v : V
⊢ v ∈ ↑s.direction ↔ v ∈ (fun x ↦ p -ᵥ x) '' ↑s

Tactic:
SetLike.mem_coe,

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
hp : p ∈ s
v : V
⊢ v ∈ s.direction ↔ v ∈ (fun x ↦ p -ᵥ x) '' ↑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₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : (↑s₁ ∩ ↑s₂).Nonempty
⊢ s₁ = s₂

Tactic:
ext p
  have hq1 := Set.mem_of_mem_inter_left hn.some_mem
  have hq2 := Set.mem_of_mem_inter_right hn.some_mem
  constructor
  · intro hp
    rw [← vsub_vadd p hn.some]
    refine vadd_mem_of_mem_direction ?_ hq2
    rw [← hd]
    exact vsub_mem_direction hp hq1
  · intro hp
    rw [← vsub_vadd p hn.some]
    refine vadd_mem_of_mem_direction ?_ hq1
    rw [hd]
    exact vsub_mem_direction hp hq2

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
⊢ balancedCoreAux 𝕜 ∅ = ∅

Tactic:
simp_rw [balancedCoreAux, iInter₂_eq_empty_iff, smul_set_empty]
  exact fun _ => ⟨1, norm_one.ge, notMem_empty _⟩

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
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : s₁.direction ⊔ s₂.direction = ⊤
h : ¬(↑s₁ ∩ ↑s₂).Nonempty
⊢ False

Tactic:
rw [Set.not_nonempty_iff_eq_empty] at h

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h1 : (↑s₁).Nonempty
h2 : (↑s₂).Nonempty
hd : s₁.direction ⊔ s₂.direction = ⊤
h : ↑s₁ ∩ ↑s₂ = ∅
⊢ False
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:
← nhds_prod_eq,

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 ↦ id i.1 ×ˢ id i.2
⊢ Absorbs 𝕜 U s
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
α : Type u_6
f : α → E
s : Set α
⊢ Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∃ r, ∀ x ∈ s, ‖f x‖ ≤ r

Tactic:
by
  simp_rw [isVonNBounded_iff', Set.forall_mem_image]

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

Goal state before:
pp: case refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
v : V
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : p -ᵥ p₂ - (p -ᵥ p₁) = v
⊢ p -ᵥ p₂ - (p -ᵥ p₁) ∈ ↑(Submodule.span k ((fun x ↦ p -ᵥ x) '' s))

Tactic:
SetLike.mem_coe,

Goal state after:
case refine_1
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
v : V
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : p -ᵥ p₂ - (p -ᵥ p₁) = v
⊢ p -ᵥ p₂ - (p -ᵥ p₁) ∈ Submodule.span k ((fun x ↦ p -ᵥ x) '' s)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

Goal state before:
pp: case refine_1
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
v : V
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : p₁ -ᵥ p - (p₂ -ᵥ p) = v
⊢ p₁ -ᵥ p - (p₂ -ᵥ p) ∈ ↑(Submodule.span k ((fun x ↦ x -ᵥ p) '' s))

Tactic:
SetLike.mem_coe,

Goal state after:
case refine_1
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
v : V
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : p₁ -ᵥ p - (p₂ -ᵥ p) = v
⊢ p₁ -ᵥ p - (p₂ -ᵥ p) ∈ Submodule.span k ((fun x ↦ x -ᵥ 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
| vectorSpan k s

Tactic:
vectorSpan_eq_span_vsub_set_left k 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) '' s)
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:
sum_smul_vsub_eq_weightedVSubOfPoint_sub,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p₁ : ι → P
p₂ b : P
⊢ (s.weightedVSubOfPoint p₁ ?b) w - (s.weightedVSubOfPoint (fun i ↦ p₂) ?b) w =
    (s.weightedVSubOfPoint p₁ b) w - (∑ i ∈ s, w i) • (p₂ -ᵥ b)

case b
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
⊢ P