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

Goal state before:
pp: n : ℕ
⊢ sin (π / 2 ^ (n + 1)) ^ 2 = 1 - (sqrtTwoAddSeries 0 n / 2) ^ 2

Tactic:
by
  rw [sin_sq, cos_pi_over_two_pow]

Goal state after:
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
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
hr : r ∈ closedBall 0 (ε / R)
⊢ {x} + r • s ⊆ u

Tactic:
simp only [image_add_left, singleton_add]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
hr : r ∈ closedBall 0 (ε / R)
⊢ (fun x_1 ↦ -x + x_1) ⁻¹' (r • s) ⊆ u
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
⊢ Summable fun n ↦ ‖↑n ^ k * r ^ n‖

Tactic:
simp only [← cast_pow]
  exact summable_norm_mul_geometric_of_norm_lt_one (k := k) (u := fun n ↦ n ^ k) hr
    (isBigO_refl _ _)

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

Goal state before:
pp: case zero
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
⊢ HasSum (fun n ↦ ↑((n + 0).choose 0) * r ^ n) ((1 - r)⁻¹ʳ ^ (0 + 1))

Tactic:
simpa using hasSum_geom_series_inverse r hr

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

Goal state before:
pp: ⊢ Function.Antiperiodic (fun x ↦ cexp (x * I)) ↑π

Tactic:
by
  simpa only [mul_inv_cancel_right₀ I_ne_zero] using exp_antiperiodic.mul_const I_ne_zero

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

Goal state before:
pp: ⊢ cexp (↑π / 2 * I) = I

Tactic:
← cos_add_sin_I,

Goal state after:
⊢ cos (↑π / 2) + sin (↑π / 2) * I = I
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cexp (-↑π / 2 * I) = -I

Tactic:
← cos_add_sin_I,

Goal state after:
⊢ cos (-↑π / 2) + sin (-↑π / 2) * I = -I
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
⊢ 𝓝 f = ⨅ K, ⨅ (_ : IsCompact K), ⨅ U, ⨅ (_ : IsOpen[inst✝] U), ⨅ (_ : MapsTo (⇑f) K U), 𝓟 {g | MapsTo (⇑g) K U}

Tactic:
by
  simp_rw +instances [compactOpen_eq, nhds_generateFrom, mem_ofPred_eq, @and_comm (f ∈ _), iInf_and,
    ← image_prod, iInf_image, biInf_prod, mem_ofPred_eq]

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

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n ↦ (↑n + 1) * x ^ n) ((1 - x)⁻¹ʳ ^ 2)
B : HasSum (fun n ↦ x ^ n) (1 - x)⁻¹ʳ
⊢ (1 - x)⁻¹ʳ ^ 2 - (1 - x) * (1 - x)⁻¹ʳ * (1 - x)⁻¹ʳ = x * (1 - x)⁻¹ʳ ^ 2

Tactic:
noncomm_ring

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
⊢ Continuous[instTopologicalSpaceProd, _] fun p ↦ (const Y p.1).prodMk p.2

Tactic:
continuous_iff_continuousAt,

Goal state after:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
⊢ ∀ (x : X × C(Y, Z)), ContinuousAt (fun p ↦ (const Y p.1).prodMk p.2) x
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactPair Y Z
⊢ Continuous fun x ↦ x.2.comp x.1

Tactic:
continuous_iff_continuousAt,

Goal state after:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactPair Y Z
⊢ ∀ (x : C(X, Y) × C(Y, Z)), ContinuousAt (fun x ↦ x.2.comp x.1) x
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace T
K : Set X
U : Set Y
inst✝ : LocallyCompactPair X Y
⊢ Continuous[instTopologicalSpaceProd, inst✝³] fun fx ↦ fx.1 fx.2

Tactic:
continuous_iff_continuousAt,

Goal state after:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace T
K : Set X
U : Set Y
inst✝ : LocallyCompactPair X Y
⊢ ∀ (x : C(X, Y) × X), ContinuousAt (fun fx ↦ fx.1 fx.2) x
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
⊢ Summable f

Tactic:
by
  by_cases! hr₀ : 0 ≤ r
  · rw [eventually_atTop] at h
    rcases h with ⟨N, hN⟩
    rw [← @summable_nat_add_iff α _ _ _ _ N]
    refine .of_norm_bounded (g := fun n ↦ ‖f N‖ * r ^ n)
      (Summable.mul_left _ <| summable_geometric_of_lt_one hr₀ hr₁) fun n ↦ ?_
    conv_rhs => rw [mul_comm, ← zero_add N]
    refine le_geom (u := fun n ↦ ‖f (n + N)‖) hr₀ n fun i _ ↦ ?_
    convert! hN (i + N) (N.le_add_left i) using 3
    ac_rfl
  · refine .of_norm_bounded_eventually_nat summable_zero ?_
    filter_upwards [h] with _ hn
    by_contra! h
    exact not_lt.mpr (norm_nonneg _) (lt_of_le_of_lt hn <| mul_neg_of_neg_of_pos hr₀ h)

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i ↦ restrict s (F i)) l (𝓝 (f s a))
s₁ : Set X
hs₁ : IsCompact s₁
s₂ : Set X
hs₂ : IsCompact s₂
x : X
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
this✝ : CompactSpace ↑s₁
this : CompactSpace ↑s₂
h₁ : Tendsto ((fun f ↦ f ⟨x, hxs₁⟩) ∘ fun i ↦ restrict s₁ (F i)) l (𝓝 ((f s₁ hs₁) ⟨x, hxs₁⟩))
⊢ (f s₁ hs₁) ⟨x, hxs₁⟩ = (f s₂ hs₂) ⟨x, hxs₂⟩

Tactic:
have h₂ := (continuous_eval_const (⟨x, hxs₂⟩ : s₂)).continuousAt.tendsto.comp (hf s₂ hs₂)

Goal state after:
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i ↦ restrict s (F i)) l (𝓝 (f s a))
s₁ : Set X
hs₁ : IsCompact s₁
s₂ : Set X
hs₂ : IsCompact s₂
x : X
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
this✝ : CompactSpace ↑s₁
this : CompactSpace ↑s₂
h₁ : Tendsto ((fun f ↦ f ⟨x, hxs₁⟩) ∘ fun i ↦ restrict s₁ (F i)) l (𝓝 ((f s₁ hs₁) ⟨x, hxs₁⟩))
h₂ : Tendsto ((fun f ↦ f ⟨x, hxs₂⟩) ∘ fun i ↦ restrict s₂ (F i)) l (𝓝 ((f s₂ hs₂) ⟨x, hxs₂⟩))
⊢ (f s₁ hs₁) ⟨x, hxs₁⟩ = (f s₂ hs₂) ⟨x, hxs₂⟩
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case snoc.snoc
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
n : ℕ
p : Fin n → X
y : X
hp₂ : ∀ (x : X), (∀ (i : Fin n), p i ∈ s) → x ∈ s → ∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin n), p i ∈ range ⇑γ
x : X
hp : ∀ (i : Fin (n + 1)), snoc p y i ∈ s
hx : x ∈ s
⊢ ∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), snoc p y i ∈ range ⇑γ

Tactic:
| @snoc n p y hp₂ =>

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
T : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace T
s : Set T
t : Set X
f : T → X → Y
g : C(↑t, Y)
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
this : ∀ x ∈ s, ContinuousOn (f x) t
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] (Function.uncurry fun x y ↦ (mkD (t.domRestrict (f ↑x)) g) y)

Tactic:
conv in mkD _ _ => rw [mkD_of_continuousOn (this x x.2)]

Goal state after:
X : Type u_2
Y : Type u_3
T : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace T
s : Set T
t : Set X
f : T → X → Y
g : C(↑t, Y)
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
this : ∀ x ∈ s, ContinuousOn (f x) t
⊢ Continuous[instTopologicalSpaceProd, inst✝¹]
    (Function.uncurry fun x y ↦ { toFun := t.domRestrict (f ↑x), continuous_toFun := ⋯ } y)
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p x : ℝ
⊢ ‖↑x‖ = ‖↑x‖

Tactic:
suffices ‖(↑(-1 * x) : AddCircle (-1 * p))‖ = ‖(x : AddCircle p)‖ by
    rw [← this, neg_one_mul]
    simp

Goal state after:
p x : ℝ
⊢ ‖↑(-1 * x)‖ = ‖↑x‖
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case refine_1
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n ↦ b * ∑ i ∈ Finset.range n, (f i.succ - f i)

Tactic:
apply Real.uniformContinuous_const_mul.comp_cauchySeq

Goal state after:
case refine_1
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b
⊢ CauchySeq fun n ↦ ∑ i ∈ Finset.range n, (f i.succ - f i)
Module: Mathlib.Analysis.Normed.Group.AddCircle

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

Tactic:
by
  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.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
⊢ γ.truncate 0 0 = (refl a).cast ⋯ ⋯

Tactic:
convert! γ.truncate_self 0

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

Goal state before:
pp: case neg.mpr
x : ℝ
h : x < 0
h₀ : ¬{ re := x, im := 0 } = 0
⊢ { re := x, im := 0 }.arg = π

Tactic:
rw [← arg_neg_one, ← arg_real_mul (-1) (neg_pos.2 h)]

Goal state after:
case neg.mpr
x : ℝ
h : x < 0
h₀ : ¬{ re := x, im := 0 } = 0
⊢ { re := x, im := 0 }.arg = (↑(-x) * -1).arg
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: l : List ℝ
h : ∀ x ∈ l, x ≠ 0
⊢ log l.prod = (List.map (fun x ↦ log x) l).sum

Tactic:
induction l with
  | nil => simp
  | cons a l ih =>
    simp_all only [ne_eq, mem_cons, or_true, not_false_eq_true, forall_const, forall_eq_or_imp,
      prod_cons, map_cons, sum_cons]
    have : l.prod ≠ 0 := by grind [prod_ne_zero]
    rw [log_mul h.1 this, add_right_inj, ih]

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

Goal state before:
pp: s : Multiset ℝ
h : ∀ x ∈ s, x ≠ 0
⊢ ∀ x ∈ s.toList, x ≠ 0

Tactic:
by simp_all

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

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ x ∈ s, f x ≠ 0
⊢ ∀ x ∈ List.map (fun i ↦ f i) s.toList, x ≠ 0

Tactic:
by simp_all

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

Goal state before:
pp: x y z : ℂ
hx : x ≠ 0
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
simp only [cpow_def, ite_mul, mul_ite]

Goal state after:
x y z : ℂ
hx : x ≠ 0
⊢ (if x = 0 then if y + z = 0 then 1 else 0 else cexp (log x * (y + z))) =
    if x = 0 then
      if z = 0 then if x = 0 then if y = 0 then 1 * 1 else 0 * 1 else cexp (log x * y) * 1
      else if x = 0 then if y = 0 then 1 * 0 else 0 * 0 else cexp (log x * y) * 0
    else
      if x = 0 then if y = 0 then 1 * cexp (log x * z) else 0 * cexp (log x * z)
      else cexp (log x * y) * cexp (log x * 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 cexp ((if x.arg = π then -(starRingEnd ℂ) (log x) else -log x) * n)) =
    if x.arg = π then (starRingEnd ℂ) (if x = 0 then if n = 0 then 1 else 0 else cexp (log x * (starRingEnd ℂ) n))⁻¹
    else (if x = 0 then if n = 0 then 1 else 0 else cexp (log x * n))⁻¹

Tactic:
ite_mul,

Goal state after:
x n : ℂ
⊢ (if x = 0 then if n = 0 then 1 else 0 else cexp (if x.arg = π then -(starRingEnd ℂ) (log x) * n else -log x * n)) =
    if x.arg = π then (starRingEnd ℂ) (if x = 0 then if n = 0 then 1 else 0 else 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✝ : ℝ
⊢ toIocMod two_pi_pos (-π) (↑x✝).toReal = (↑x✝).toReal

Tactic:
toReal_coe

Goal state after:
case h
x✝ : ℝ
⊢ toIocMod two_pi_pos (-π) (toIocMod two_pi_pos (-π) x✝) = toIocMod two_pi_pos (-π) x✝
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ (↑π).sign = 0

Tactic:
by rw [sign, sin_coe_pi, _root_.sign_zero]

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

Goal state before:
pp: θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ 0 ≤ (↑θ).sign

Tactic:
rw [sign, sign_nonneg_iff]
  exact sin_nonneg_of_nonneg_of_le_pi h0 hpi

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
⊢ a = b

Tactic:
rw [Real.Angle.sign_add_pi] at this

Goal state after:
case mp.inr
a b : Angle
ha : a.sign ≠ 0
h : a.sign = b.sign
h2 : a = b + ↑π
this : a.sign = -b.sign
⊢ a = b
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
hne : ↑x ≠ 0
⊢ cexp ((↑(Real.log ‖↑x‖) + ↑(↑x).arg * I) * y) = cexp ((↑(Real.log ‖↑x‖) + ↑(-↑x).arg * I + ↑π * I) * y)

Tactic:
arg_ofReal_of_neg hlt,

Goal state after:
case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
hne : ↑x ≠ 0
⊢ cexp ((↑(Real.log ‖↑x‖) + ↑π * I) * y) = cexp ((↑(Real.log ‖↑x‖) + ↑(-↑x).arg * I + ↑π * I) * y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: ι : Type u_1
l : List ι
f : ι → ℝ≥0
r : ℝ
⊢ (List.map (fun x ↦ f x ^ r) l).prod = (List.map f l).prod ^ r

Tactic:
rw [← list_prod_map_rpow, List.map_map]; rfl

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

Goal state before:
pp: x : ℝ
hx : x ≠ 0
y z : ℝ≥0
hyz : (fun y ↦ y ^ x) y = (fun y ↦ y ^ x) z
⊢ y = z

Tactic:
simpa only [rpow_inv_rpow_self hx] using congr_arg (fun y => y ^ (1 / x)) hyz

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

Goal state before:
pp: case inr.inr
x : ℝ≥0
y z : ℝ
hx₀ : x ≠ 0
hx₁ : x ≠ 1
⊢ x ^ y = x ^ z ↔ y = z ∨ x = 1 ∨ x = 0 ∧ (y = 0 ↔ z = 0)

Tactic:
simpa [hx₀, hx₁] using rpow_right_inj (y := y) (z := z) hx₀ hx₁

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

Goal state before:
pp: x : ℝ
⊢ 1 ^ x = 1

Tactic:
rw [← coe_one, ← coe_rpow_of_ne_zero one_ne_zero]

Goal state after:
x : ℝ
⊢ ↑(1 ^ x) = ↑1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: r : ℝ
s : Set ℝ≥0
h : 0 ∉ s ∨ 0 ≤ r
x✝ : 0 ∉ s
⊢ s ⊆ {0}ᶜ

Tactic:
by simp_all

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

Goal state before:
pp: x y : ℝ
h₁ : 0 ≤ x
h₂ : x ≤ 1
h₃ : y ≤ 1
⊢ x ≤ x ^ y

Tactic:
by
  simpa only [rpow_one]
    using rpow_le_rpow_of_exponent_ge_of_imp h₁ h₂ h₃ fun _ ↦ (absurd · one_ne_zero)

Goal state after:
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 ^ x) ^ x⁻¹ = (z ^ x) ^ x⁻¹

Tactic:
hyz

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

Goal state before:
pp: case insert
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
i : ι
s : Finset ι
hi : i ∉ s
ih : (∀ i ∈ s, f i ≠ ∞) → ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r
hf : ∀ i_1 ∈ insert i s, f i_1 ≠ ∞
⊢ ∏ i ∈ insert i s, f i ^ r = (∏ i ∈ insert i s, f i) ^ r

Tactic:
have h2f : ∀ i ∈ s, f i ≠ ∞ := fun i hi ↦ hf i <| mem_insert_of_mem hi

Goal state after:
case insert
ι : Type u_1
f : ι → ℝ≥0∞
r : ℝ
i : ι
s : Finset ι
hi : i ∉ s
ih : (∀ i ∈ s, f i ≠ ∞) → ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r
hf : ∀ i_1 ∈ insert i s, f i_1 ≠ ∞
h2f : ∀ i ∈ s, f i ≠ ∞
⊢ ∏ i ∈ insert i s, f i ^ r = (∏ i ∈ insert i s, f i) ^ r
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

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

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

Tactic:
← sqrt_mul,

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

case hx
x : ℂ
⊢ 0 ≤ ‖x‖

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

case hr
x : ℂ
⊢ x.arg ≤ π
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
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : RayVector R M
hxy : SameRay R ↑((equiv R M) x) ↑((equiv R M) y)
⊢ SameRay R ↑((equiv R M) y) ↑((equiv R M) z) → SameRay R ↑((equiv R M) x) ↑((equiv R M) z)

Tactic:
hyz

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : IsStrictOrderedRing R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : RayVector R M
hxy : SameRay R ↑((equiv R M) x) ↑((equiv R M) y)
hyz : SameRay R ↑((equiv R M) y) ↑((equiv R M) z)
⊢ SameRay R ↑((equiv R M) x) ↑((equiv R M) z)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V1
inst✝³ : AffineSpace V1 P1
inst✝² : Module k V1
ι : Type u_9
φv : ι → Type u_10
inst✝¹ : (i : ι) → AddCommGroup (φv i)
inst✝ : (i : ι) → Module k (φv i)
fv : (i : ι) → P1 →ᵃ[k] φv i
⊢ pi fv = 0 ↔ ∀ (i : ι), fv i = 0

Tactic:
simp only [AffineMap.ext_iff, funext_iff, pi_apply]
  exact forall_comm

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] = ⇑(AffineMap.lineMap x y) '' Icc 0 1

Tactic:
convert segment_eq_image 𝕜 x y

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Icc 0 1
⊢ (AffineMap.lineMap x y) a✝¹ = (1 - a✝¹) • x + a✝¹ • y
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 q : AffineSubspace k P
x✝ : p.carrier = q.carrier
⊢ p = q

Tactic:
by cases p; cases q; congr

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 : 𝕜
hxy : x ≠ y
h : y < x
⊢ Ioo y x = Ioo (min x y) (max x y)

Tactic:
max_eq_left h.le,

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
hxy : x ≠ y
h : y < x
⊢ Ioo y x = Ioo (min x y) x
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : IsOrderedRing 𝕜
x y : E
ap bp : 𝕜
hap : 0 ≤ ap
hbp : 0 ≤ bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 ≤ aq
hbq : 0 ≤ bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a * ap + b * aq) * 1 = a * (ap * 1) + b * (aq * 1)

Tactic:
noncomm_ring

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : IsOrderedRing 𝕜
x y : E
ap bp : 𝕜
hap : 0 ≤ ap
hbp : 0 ≤ bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 ≤ aq
hbq : 0 ≤ bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a * bp + b * bq) * 1 = a * (bp * 1) + b * (bq * 1)

Tactic:
noncomm_ring

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

Goal state before:
pp: case refine_2.inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
ha' : 0 < a
⊢ a * x + b * y ∈ Ioc x y

Tactic:
exact Ioo_subset_Ioc_self ((Convex.mem_Ioo h).2 ⟨a, b, ha', hb, hab, rfl⟩)

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

Goal state before:
pp: case a
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : CommSemiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a✝ b✝ : E
ap bp : 𝕜
hap : 0 < ap
hbp : 0 < bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 < aq
hbq : 0 < bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a * ap + b * aq + (a * bp + b * bq) + (a * 1 + b * 1 + 1) = 1 + (a * (ap + bp) + b * (aq + bq) + (a + b))

Tactic:
noncomm_ring

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : AddRightMono 𝕜
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : x + y ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
⊢ 1 = (1 - t) * 1 + t * 1

Tactic:
noncomm_ring

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : AddRightMono 𝕜
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : x + y ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
⊢ t * 1 = t * 1

Tactic:
noncomm_ring

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

Goal state before:
pp: 𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁷ : NormedDivisionRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
s : Set E
inst✝⁴ : NormedRing 𝕝
inst✝³ : Module 𝕜 𝕝
inst✝² : NormSMulClass 𝕜 𝕝
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
⊢ ‖b⁻¹ • a‖ ≤ 1

Tactic:
rw [norm_smul, norm_inv, ← div_eq_inv_mul]

Goal state after:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁷ : NormedDivisionRing 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
s : Set E
inst✝⁴ : NormedRing 𝕝
inst✝³ : Module 𝕜 𝕝
inst✝² : NormSMulClass 𝕜 𝕝
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
⊢ ‖a‖ / ‖b‖ ≤ 1
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁸ : NormedDivisionRing 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
s : Set E
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : Module 𝕜 𝕝
inst✝³ : NormSMulClass 𝕜 𝕝
inst✝² : SMulWithZero 𝕝 E
inst✝¹ : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst✝ : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
⊢ ‖a⁻¹ • b‖ ≤ 1

Tactic:
rw [norm_smul, norm_inv, ← div_eq_inv_mul]

Goal state after:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁸ : NormedDivisionRing 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
s : Set E
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : Module 𝕜 𝕝
inst✝³ : NormSMulClass 𝕜 𝕝
inst✝² : SMulWithZero 𝕝 E
inst✝¹ : IsScalarTower 𝕜 𝕝 E
a : 𝕜
x : E
inst✝ : SMulCommClass 𝕝 𝕜 E
hs : Balanced 𝕝 s
b : 𝕝
ha : a • x ∈ s
hba : ‖b‖ ≤ ‖a‖
ha₀ : a ≠ 0
⊢ ‖b‖ / ‖a‖ ≤ 1
Module: Mathlib.Analysis.Convex.Strict

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_3
inst✝⁷ : CommSemiring 𝕜
inst✝⁶ : IsDomain 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Module.IsTorsionFree 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
h✝ : 0 ∉ s
⊢ StrictConvex 𝕜 ∅

Tactic:
· exact strictConvex_empty

Goal state after: