mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(ℑ a) = -I • 2⁻¹ • (a - star a)

Tactic:
by
  simp [imaginaryPart]

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

Goal state before:
pp: x y : ℂ
h : RCLike.re x ≤ RCLike.re y ∧ RCLike.im x = RCLike.im y
⊢ x.re ≤ y.re

Tactic:
exact h.1

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 ≤ re z ∧ im z = 0 ↔ ∃ x ≥ 0, re ↑x = re z ∧ im ↑x = im z

Tactic:
aesop

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 < re z ∧ im z = 0 ↔ ∃ x > 0, re ↑x = re z ∧ im ↑x = im z

Tactic:
aesop

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ re z ≤ 0 ∧ im z = 0 ↔ ∃ x ≤ 0, re ↑x = re z ∧ im ↑x = im z

Tactic:
aesop

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ re z < 0 ∧ im z = 0 ↔ ∃ x < 0, re ↑x = re z ∧ im ↑x = im z

Tactic:
aesop

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : K
h : re x ≤ re y ∧ im x = im y
⊢ re x ≤ re y

Tactic:
exact h.1

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ IsClosed {p | re p.1 ≤ re p.2 ∧ im p.1 = im p.2}

Tactic:
Set.ofPred_and

Goal state after:
K : Type u_1
inst✝ : RCLike K
⊢ IsClosed ({a | re a.1 ≤ re a.2} ∩ {a | im a.1 = im a.2})
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ cosh (x + y) = cosh x * cosh y + sinh x * sinh y

Tactic:
rw [← mul_right_inj' (two_ne_zero' ℂ), two_cosh, exp_add, neg_add, exp_add, eq_comm, mul_add, ←
    mul_assoc, two_cosh, ← mul_assoc, two_sinh, ← mul_right_inj' (two_ne_zero' ℂ), mul_add,
    mul_left_comm, two_cosh, mul_left_comm, two_sinh]
  exact cosh_add_aux

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ‖∑ m ∈ range j with n ≤ m, x ^ m / ↑m.factorial‖ = ‖∑ m ∈ range j with n ≤ m, x ^ n * (x ^ (m - n) / ↑m.factorial)‖

Tactic:
refine congr_arg norm (sum_congr rfl fun m hm => ?_)

Goal state after:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
m : ℕ
hm : m ∈ {m ∈ range j | n ≤ m}
⊢ x ^ m / ↑m.factorial = x ^ n * (x ^ (m - n) / ↑m.factorial)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ sin x ^ 2 = 1 - cos x ^ 2

Tactic:
by rw [← sin_sq_add_cos_sq x, add_sub_cancel_right]

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ (cexp x).im = Real.exp x.re * Real.sin x.im

Tactic:
rw [exp_eq_exp_re_mul_sin_add_cos]
  simp [exp_ofReal_re, sin_ofReal_re]

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
⊢ ‖cexp x‖ ≤ Real.exp ‖x‖

Tactic:
convert norm_exp_sub_sum_le_exp_norm_sub_sum x 0 <;> simp

Goal state after:
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖∑ m ∈ Ico n j, x ^ m / ↑m.factorial‖ = ‖∑ m ∈ Ico n j, x ^ n * (x ^ (m - n) / ↑m.factorial)‖

Tactic:
refine congr_arg norm (sum_congr rfl fun m hm => ?_)

Goal state after:
x : ℂ
n j : ℕ
hj : j ≥ n
m : ℕ
hm : m ∈ Ico n j
⊢ x ^ m / ↑m.factorial = x ^ n * (x ^ (m - n) / ↑m.factorial)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
m : ℕ
hm : m ∈ Ico n j
⊢ x ^ m / ↑m.factorial = x ^ n * (x ^ (m - n) / ↑m.factorial)

Tactic:
mem_Ico

Goal state after:
x : ℂ
n j : ℕ
hj : j ≥ n
m : ℕ
hm : n ≤ m ∧ m < j
⊢ x ^ m / ↑m.factorial = x ^ n * (x ^ (m - n) / ↑m.factorial)
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
k : ℤ
h : k + k ≠ 0
⊢ 0 < a ^ (k + k) ↔ a ≠ 0

Tactic:
rw [zpow_add' (by simp [em']), mul_self_pos, zpow_ne_zero_iff (by simpa using h)]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: case inl
b c : ℝ
hb : 0 < b
⊢ Tendsto (fun x ↦ (b * rexp x + c) / x ^ 0) atTop atTop

Tactic:
simp only [pow_zero, div_one]
    exact (tendsto_exp_atTop.const_mul_atTop hb).atTop_add tendsto_const_nhds

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

Goal state before:
pp: x : ℝ
hx₁ : -π < x
hx₂ : x < π
h : sin x = 0
⊢ x = 0

Tactic:
by
    contrapose! h
    cases h.lt_or_gt with
    | inl h0 => exact (sin_neg_of_neg_of_neg_pi_lt h0 hx₁).ne
    | inr h0 => exact (sin_pos_of_pos_of_lt_pi h0 hx₂).ne'

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ {x} * (closedBall y δ)⁻¹ = closedBall (x * y⁻¹) δ

Tactic:
inv_closedBall,

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ {x} * closedBall y⁻¹ δ = closedBall (x * y⁻¹) δ
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: case inr
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, f x = 0
x : M ⧸ S
h : 0 < ‖f‖
⊢ ¬‖x‖ < ‖(lift S f.toAddMonoidHom hf) x‖ / ‖f‖

Tactic:
norm_lt_iff

Goal state after:
case inr
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, f x = 0
x : M ⧸ S
h : 0 < ‖f‖
⊢ ¬∃ m, ↑m = x ∧ ‖m‖ < ‖(lift S f.toAddMonoidHom hf) x‖ / ‖f‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℕ
⊢ sqrtTwoAddSeries 0 (n + 1) < 2

Tactic:
by
    refine lt_of_lt_of_le ?_ (sqrt_sq zero_lt_two.le).le
    rw [sqrtTwoAddSeries, sqrt_lt_sqrt_iff, ← lt_sub_iff_add_lt']
    · refine (sqrtTwoAddSeries_lt_two n).trans_le ?_
      norm_num
    · exact add_nonneg zero_le_two (sqrtTwoAddSeries_zero_nonneg n)

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

Goal state before:
pp: case h
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ 0 ≤ r

Tactic:
exact h.1

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

Goal state before:
pp: ⊢ cos (π / 4) = cos (π / 2 ^ 2)

Tactic:
congr
    norm_num

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

Goal state before:
pp: ⊢ sin (π / 4) = sin (π / 2 ^ 2)

Tactic:
congr
    norm_num

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

Goal state before:
pp: ⊢ cos (π / 8) = cos (π / 2 ^ 3)

Tactic:
congr
    norm_num

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

Goal state before:
pp: case neg
k : ℕ
r : ℝ
hr : |r| < 1
h0 : ¬r = 0
hr' : 1 < |r|⁻¹
⊢ Tendsto (fun n ↦ ↑n ^ k * r ^ n) atTop (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]

Goal state after:
case neg
k : ℕ
r : ℝ
hr : |r| < 1
h0 : ¬r = 0
hr' : 1 < |r|⁻¹
⊢ Tendsto (fun x ↦ ‖↑x ^ k * r ^ x‖) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 8) = sin (π / 2 ^ 3)

Tactic:
congr
    norm_num

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

Goal state before:
pp: ⊢ cos (π / 16) = cos (π / 2 ^ 4)

Tactic:
congr
    norm_num

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

Goal state before:
pp: ⊢ sin (π / 16) = sin (π / 2 ^ 4)

Tactic:
congr
    norm_num

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

Goal state before:
pp: ⊢ cos (π / 32) = cos (π / 2 ^ 5)

Tactic:
congr
    norm_num

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

Goal state before:
pp: ⊢ sin (π / 32) = sin (π / 2 ^ 5)

Tactic:
congr
    norm_num

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

Goal state before:
pp: ⊢ cos (π / 3) = 1 / 2

Tactic:
have h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0 := by
    have : cos (3 * (π / 3)) = cos π := by
      congr 1
      ring
    linarith [cos_pi, cos_three_mul (π / 3)]

Goal state after:
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
⊢ cos (π / 3) = 1 / 2
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
R✝ : Type u_2
S : Type u_3
inst✝⁷ : Field R✝
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
v w : AbsoluteValue R✝ S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
_i : OrderTopology S
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
hx : ‖x‖ < 1
h1 : Summable fun n ↦ ‖x‖ ^ n
⊢ Summable fun n ↦ x ^ n

Tactic:
exact h1.of_norm_bounded_eventually_nat (eventually_norm_pow_le x)

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
F : Set X
hxy : JoinedIn F x y
hyz : JoinedIn F y z
⊢ JoinedIn F x z

Tactic:
obtain ⟨hx, hy⟩ := hxy.mem

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
F : Set X
hxy : JoinedIn F x y
hyz : JoinedIn F y z
hx : x ∈ F
hy : y ∈ F
⊢ JoinedIn F x z
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := ⋯
⊢ PathConnectedSpace X → Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)

pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := ⋯
⊢ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X) → PathConnectedSpace X

Tactic:
· intro h
    refine ⟨(nonempty_quotient_iff _).mpr h.1, ⟨?_⟩⟩
    rintro ⟨x⟩ ⟨y⟩
    exact Quotient.sound (PathConnectedSpace.joined x y)

Goal state after:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := ⋯
⊢ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X) → PathConnectedSpace X
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : IsPathConnected s
ht : IsPathConnected t
⊢ IsPathConnected (s ×ˢ t)

Tactic:
rw [isPathConnected_iff]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : IsPathConnected s
ht : IsPathConnected t
⊢ (s ×ˢ t).Nonempty ∧ ∀ x ∈ s ×ˢ t, ∀ y ∈ s ×ˢ t, JoinedIn (s ×ˢ t) x y
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ₁ : Path x y
γ₂ : Path y z
t : ℝ
ht : 1 / 2 ≤ t
⊢ (γ₁.trans γ₂).extend t = γ₂.extend (2 * t - 1)

Tactic:
by
  conv_lhs => rw [← sub_sub_cancel 1 t]
  rw [← extend_symm_apply, trans_symm, extend_trans_of_le_half _ _ (by linarith), extend_symm_apply]
  congr 1
  linarith

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

Goal state before:
pp: case e_s
p x t : ℝ
ht : t ≠ 0
m : ℝ
⊢ m ∈ {m | ↑m = ↑(t * x)} ↔ m ∈ t • {m | ↑m = ↑x}

Tactic:
eq_iff_sub_mem,

Goal state after:
case e_s
p x t : ℝ
ht : t ≠ 0
m : ℝ
⊢ m ∈ {m | m - t * x ∈ { carrier := range fun x ↦ x • (t * p), add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }} ↔
    m ∈ t • {m | m - x ∈ { carrier := range fun x ↦ x • p, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }}
Module: Mathlib.Topology.Instances.AddCircle.Real

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
⊢ Injective ⇑toAddCircle

Tactic:
by
  intro x y hxy
  have : (0 : ℝ) < N := Nat.cast_pos.mpr (NeZero.pos _)
  rwa [toAddCircle_apply, toAddCircle_apply, AddCircle.coe_eq_coe_iff_of_mem_Ico,
    div_left_inj' this.ne', Nat.cast_inj, (val_injective N).eq_iff] at hxy <;>
  exact ⟨by positivity, by simpa only [zero_add, div_lt_one this, Nat.cast_lt] using val_lt _⟩

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

Goal state before:
pp: x y θ : ℝ
hθ : θ ∈ Icc (-(π / 2)) (π / 2)
⊢ -(π / 2) ≤ θ

Tactic:
aesop

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

Goal state before:
pp: x y θ : ℝ
hθ : θ ∈ Icc (-(π / 2)) (π / 2)
⊢ θ ≤ π / 2

Tactic:
aesop

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

Goal state before:
pp: x✝ y x : ℝ
hx : x ∈ Icc (-1) 1
⊢ -1 ≤ x

Tactic:
aesop

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

Goal state before:
pp: x✝ y x : ℝ
hx : x ∈ Icc (-1) 1
⊢ x ≤ 1

Tactic:
aesop

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

Goal state before:
pp: x y θ : ℝ
hθ : θ ∈ Icc 0 π
⊢ 0 ≤ θ

Tactic:
aesop

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

Goal state before:
pp: x y θ : ℝ
hθ : θ ∈ Icc 0 π
⊢ θ ≤ π

Tactic:
aesop

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

Goal state before:
pp: case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ z.arg ≤ π / 2 ↔ False

Tactic:
rw [iff_false, not_le, arg_of_re_neg_of_im_nonneg hre him, ← sub_lt_iff_lt_add, half_sub,
      Real.neg_pi_div_two_lt_arcsin, neg_im, neg_div, neg_lt_neg_iff, div_lt_one, ←
      abs_of_nonneg him, abs_im_lt_norm]

Goal state after:
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ z.re ≠ 0

case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ 0 < ‖z‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inl.inr.inr
x : ℂ
hi : x.im = 0
hr : 0 < x.re
⊢ (-↑x.re).arg = (↑x.re).arg - π ↔ 0 < (↑x.re).im ∨ (↑x.re).im = 0 ∧ (↑x.re).re < 0

Tactic:
· rw [arg_ofReal_of_nonneg hr.le, ← ofReal_neg, arg_ofReal_of_neg (Left.neg_neg_iff.2 hr)]
      simp [hr.not_gt, ← add_eq_zero_iff_eq_neg, Real.pi_ne_zero]

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

Goal state before:
pp: case inr
ψ : Angle
⊢ |(ψ + ↑π).sin| = |ψ.sin|

Tactic:
sin_add_pi,

Goal state after:
case inr
ψ : Angle
⊢ |(-ψ.sin)| = |ψ.sin|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : ℝ
⊢ toIcoMod two_pi_pos ψ θ - θ = 2 * π * ↑(-toIcoDiv two_pi_pos ψ θ)

Tactic:
toIcoMod_sub_self,

Goal state after:
θ ψ : ℝ
⊢ -toIcoDiv two_pi_pos ψ θ • (2 * π) = 2 * π * ↑(-toIcoDiv two_pi_pos ψ θ)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ SignType.sign (θ + ↑π).sin = -SignType.sign θ.sin

Tactic:
sin_add_pi,

Goal state after:
θ : Angle
⊢ SignType.sign (-θ.sin) = -SignType.sign θ.sin
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
aesop

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 + ↑π
this✝ : a.sign = -b.sign
this : (a.sign = b.sign) = (-b.sign = b.sign)
⊢ a = b

Tactic:
aesop

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

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

Tactic:
aesop

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

Goal state before:
pp: b : ℝ
hb : 1 < b
⊢ 1 < b

Tactic:
aesop

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

Goal state before:
pp: l : List ℝ
hl : ∀ x ∈ l, 0 ≤ x
r : ℝ
⊢ (List.map (fun x ↦ x ^ r) l).prod = l.prod ^ r

Tactic:
lift l to List ℝ≥0 using hl
  have := congr_arg ((↑) : ℝ≥0 → ℝ) (NNReal.list_prod_map_rpow l r)
  push_cast at this
  rw [List.map_map] at this ⊢
  exact mod_cast this

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

Goal state before:
pp: y : ℝ
x : ℝ≥0∞
hx : 0 < x
hx' : x ≠ ∞
h : x ^ y = ∞
⊢ False

Tactic:
simp [rpow_eq_top_iff, hx.ne', hx'] at h

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

Goal state before:
pp: x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x < y ^ z⁻¹ ↔ x ^ z < y

Tactic:
by
  nth_rw 1 [← rpow_one x]
  nth_rw 1 [← @mul_inv_cancel₀ _ _ z (ne_of_lt hz).symm]
  rw [rpow_mul, @rpow_lt_rpow_iff _ _ z⁻¹ (by simp [hz])]

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

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

Tactic:
exact (arg_neg_iff.2 hx).le

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

Goal state before:
pp: b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ
⊢ a ^ (-Int.ofNat n) = (a ^ n)⁻¹

Tactic:
zpow_neg,

Goal state after:
b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ
⊢ (a ^ Int.ofNat n)⁻¹ = (a ^ n)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ≥0
⊢ a ^ (-Int.ofNat n) = (a ^ n)⁻¹

Tactic:
zpow_neg,

Goal state after:
b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ≥0
⊢ (a ^ Int.ofNat n)⁻¹ = (a ^ n)⁻¹
Module: Mathlib.LinearAlgebra.AffineSpace.Midpoint

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ midpoint R x y +ᵥ midpoint R x y = midpoint R x y +ᵥ midpoint R y x

Tactic:
by rw [midpoint_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: 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
v : M
r : R
hv : v ≠ 0
hr : r ≠ 0
⊢ SameRay R (-v) (r • v) ↔ r < 0

Tactic:
simp only [sameRay_neg_smul_right_iff, hv, or_false, hr.le_iff_lt]

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

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
s : Set E
⊢ (∀ ⦃y : E⦄, y ∈ s → [x -[𝕜] y] ⊆ s) → StarConvex 𝕜 x s

Tactic:
rintro h y hy a b ha hb hab
    exact h hy ⟨a, b, ha, hb, hab, rfl⟩

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
inst✝ : Nontrivial 𝕜
⊢ LinearIndependent 𝕜 ![x, y] ∧ -1 * s ≠ t * -1

Tactic:
aesop

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

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
⊢ z ∈ [x -[𝕜] y]

Tactic:
refine ⟨(y - z) / (y - x), (z - x) / (y - x), div_nonneg hyz h.le, div_nonneg hxz h.le, ?_, ?_⟩

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

case inr.refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
⊢ ((y - z) / (y - x)) • x + ((z - x) / (y - x)) • y = z
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 : AffineSubspace k V
inst✝ : Nonempty ↥s
h : ↑s -ᵥ ↑s = ↑s
x : ↥s
this : ↑x - ↑x ∈ ↑s
⊢ 0 ∈ s

Tactic:
aesop

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 : AffineSubspace k V
inst✝ : Nonempty ↥s
h : ↑s -ᵥ ↑s = ↑s
x : ↥s
⊢ ∃ x_1 ∈ ↑s, ∃ y ∈ ↑s, x_1 -ᵥ y = ↑x - ↑x

Tactic:
aesop

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
v : V
hv : v ∈ s.direction
p : P
hp : p ∈ s
⊢ v +ᵥ p ∈ s

Tactic:
by
  rw [mem_direction_iff_eq_vsub ⟨p, hp⟩] at hv
  rcases hv with ⟨p₁, hp₁, p₂, hp₂, hv⟩
  rw [hv]
  convert s.smul_vsub_vadd_mem 1 hp₁ hp₂ hp
  rw [one_smul]

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

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

Tactic:
· rintro v ⟨p₂, hp₂, rfl⟩
    exact ⟨p₂, hp₂, p, hp, rfl⟩

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

Tactic:
Set.mem_image,

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
⊢ (∃ x ∈ ↑s, x -ᵥ p = -v) ↔ 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
S : AffineSpace V P
ι : Sort u_4
s : Set (AffineSubspace k P)
c : k
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ ⋂ s' ∈ s, ↑s'
hp₂ : p₂ ∈ ⋂ s' ∈ s, ↑s'
hp₃ : p₃ ∈ ⋂ s' ∈ s, ↑s'
s₂ : AffineSubspace k P
hs₂ : s₂ ∈ s
⊢ c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ ↑s₂

Tactic:
rw [Set.mem_iInter₂] at *

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
ι : Sort u_4
s : Set (AffineSubspace k P)
c : k
p₁ p₂ p₃ : P
hp₁ : ∀ i ∈ s, p₁ ∈ ↑i
hp₂ : ∀ i ∈ s, p₂ ∈ ↑i
hp₃ : ∀ i ∈ s, p₃ ∈ ↑i
s₂ : AffineSubspace k P
hs₂ : s₂ ∈ s
⊢ c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ ↑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✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : PosSMulMono 𝕜 E
x : E
s : Set E
hs : s.OrdConnected
hx : x ∈ s
h : ∀ y ∈ s, x ≤ y ∨ y ≤ x
⊢ StarConvex 𝕜 x s

Tactic:
intro y hy a b ha hb hab
  obtain hxy | hyx := h _ hy
  · refine hs.out hx hy (mem_Icc.2 ⟨?_, ?_⟩)
    · calc
        x = a • x + b • x := (Convex.combo_self hab _).symm
        _ ≤ a • x + b • y := by gcongr
    calc
      a • x + b • y ≤ a • y + b • y := by gcongr
      _ = y := Convex.combo_self hab _
  · refine hs.out hy hx (mem_Icc.2 ⟨?_, ?_⟩)
    · calc
        y = a • y + b • y := (Convex.combo_self hab _).symm
        _ ≤ a • x + b • y := by gcongr
    calc
      a • x + b • y ≤ a • x + b • x := by gcongr
      _ = x := Convex.combo_self hab _

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
S : Set (Set E)
h : ∀ s ∈ S, Balanced 𝕜 s
x✝³ : 𝕜
x✝² : ‖x✝³‖ ≤ 1
x✝¹ : E
x✝ : x✝¹ ∈ ⋂ s ∈ S, x✝³ • s
⊢ x✝¹ ∈ ⋂₀ S

Tactic:
aesop

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝² : SeminormedRing 𝕜
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s : Set F
hs : Balanced 𝕜 s
f : E →ₑ[id] F
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
x✝ : x ∈ a • ⇑f ⁻¹' s
y : E
hy₁ : y ∈ ⇑f ⁻¹' s
hy₂ : (fun x ↦ a • x) y = x
⊢ a • f y ∈ s

Tactic:
exact hs a ha (smul_mem_smul_set hy₁)

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
p₁ p₂ : P
s : AffineSubspace k P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ {p₁, p₂} ⊆ ↑s

Tactic:
Set.insert_subset_iff,

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
p₁ p₂ : P
s : AffineSubspace k P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ p₁ ∈ ↑s ∧ {p₂} ⊆ ↑s