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

Goal state before:
pp: k : ℤ
⊢ |cos (↑k * π)| = 1

Tactic:
by
  simp [abs_cos_eq_sqrt_one_sub_sin_sq]

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ s * ball 1 δ = thickening δ s

Tactic:
rw [thickening_eq_biUnion_ball]
  convert! iUnion₂_mul (fun x (_ : x ∈ s) => { x }) (ball (1 : E) δ)
  · exact s.biUnion_of_singleton.symm
  ext x
  simp_rw [singleton_mul_ball, mul_one]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ infEDist (c • x) (c • s) = ‖c‖₊ • infEDist x s

Tactic:
by
  simp_rw [infEDist]
  have : Function.Surjective ((c • ·) : E → E) :=
    Function.RightInverse.surjective (smul_inv_smul₀ hc)
  trans ⨅ (y) (_ : y ∈ s), ‖c‖₊ • edist x y
  · refine (this.iInf_congr _ fun y => ?_).symm
    simp_rw [smul_mem_smul_set_iff₀ hc, edist_smul₀]
  · have : (‖c‖₊ : ENNReal) ≠ 0 := by simp [hc]
    simp_rw [ENNReal.smul_def, smul_eq_mul, ENNReal.mul_iInf_of_ne this ENNReal.coe_ne_top]

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

Goal state before:
pp: h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
⊢ cos π < cos (π / 3)

Tactic:
refine cos_lt_cos_of_nonneg_of_le_pi ?_ le_rfl ?_

Goal state after:
case refine_1
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
⊢ 0 ≤ π / 3

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

Goal state before:
pp: case pos
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f (b + 1)‖ ≤ r * ‖f b‖
⊢ Summable f

Tactic:
rw [← @summable_nat_add_iff α _ _ _ _ N]

Goal state after:
case pos
α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
hr₀ : 0 ≤ r
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f (b + 1)‖ ≤ r * ‖f b‖
⊢ Summable fun n ↦ f (n + N)
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ∈ pathComponent y
z : X
h' : y ∈ pathComponent z
⊢ x ∈ pathComponent z

Tactic:
exact h'.trans h

Goal state after:
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_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
f g : C(X, Y)
⊢ ⇑f ⤳ ⇑g ↔ f ⤳ g

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ h.map continuous_coeFun⟩
  suffices ∀ K, IsCompact K → ∀ U, IsOpen U → MapsTo g K U → MapsTo f K U by
    simpa [specializes_iff_pure, nhds_compactOpen]
  exact fun K _ U hU hg x hx ↦ (h.map (continuous_apply x)).mem_open hU (hg hx)

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

Goal state before:
pp: case right.inl
X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
y : X
yU : y ∈ U
⊢ JoinedIn (U ∪ V) x y

Tactic:
exact (hU.joinedIn x xU y yU).mono subset_union_left

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

Goal state before:
pp: α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), N₀ ≤ b → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
⊢ ¬Summable f

Tactic:
rw [← @summable_nat_add_iff α _ _ _ _ N]

Goal state after:
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), N₀ ≤ b → r * ‖f b‖ ≤ ‖f (b + 1)‖
N : ℕ
hNN₀ : N₀ ≤ N
hN : ‖f N‖ ≠ 0
⊢ ¬Summable fun n ↦ f (n + N)
Module: Mathlib.Topology.Instances.ZMultiples

Goal state before:
pp: case inr
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ ∃ t, IsOpen t ∧ Subtype.val ⁻¹' t = {0}

Tactic:
refine ⟨ball 0 |a|, isOpen_ball, ?_⟩

Goal state after:
case inr
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ Subtype.val ⁻¹' ball 0 |a| = {0}
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case mk
p : ℝ
x✝ : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ |p⁻¹ * x - ↑(round (p⁻¹ * x)) * (p⁻¹ * p)| ≤ |p⁻¹| * (|p| / 2)

Tactic:
← mul_div_assoc,

Goal state after:
case mk
p : ℝ
x✝ : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ |p⁻¹ * x - ↑(round (p⁻¹ * x)) * (p⁻¹ * p)| ≤ |p⁻¹| * |p| / 2
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr
p : ℝ
hp : p ≠ 0
⊢ |p / 2 - ↑(round (p⁻¹ * (p / 2))) * p| = |p| / 2

Tactic:
← mul_div_assoc,

Goal state after:
case inr
p : ℝ
hp : p ≠ 0
⊢ |p / 2 - ↑(round (p⁻¹ * p / 2)) * p| = |p| / 2
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr.left
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
⊢ -(p * (1 / 2)) ≤ x

Tactic:
← mul_div_assoc,

Goal state after:
case inr.left
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
⊢ -(p * 1 / 2) ≤ x
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr.right
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
⊢ x < p * (1 / 2)

Tactic:
← mul_div_assoc,

Goal state after:
case inr.right
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
⊢ x < p * 1 / 2
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
⊢ ∑ i ∈ Finset.range (2 * k), (-1) ^ i * f i ≤ l

Tactic:
have hm : Monotone (fun n ↦ ∑ i ∈ range (2 * n), (-1) ^ i * f i) := by
    refine monotone_nat_of_le_succ (fun n ↦ ?_)
    rw [show 2 * (n + 1) = 2 * n + 1 + 1 by ring, sum_range_succ, sum_range_succ]
    simp_rw [_root_.pow_succ', show (-1 : E) ^ (2 * n) = 1 by simp, neg_one_mul, one_mul,
      ← sub_eq_add_neg, le_sub_iff_add_le]
    gcongr
    exact hfa (by lia)
  exact hm.ge_of_tendsto (hfl.comp (tendsto_atTop_mono (fun n ↦ by dsimp; lia) tendsto_id)) _

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

Goal state before:
pp: x : ℝ
⊢ π / 4 ≤ arcsin x ↔ √2 / 2 ≤ x

Tactic:
rw [← sin_pi_div_four, le_arcsin_iff_sin_le']
  have := pi_pos
  constructor <;> linarith

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

Goal state before:
pp: x : ℝ
⊢ π / 2 - arcsin (-x) = π / 2 + π / 2 - arccos x

Tactic:
arcsin_neg,

Goal state after:
x : ℝ
⊢ π / 2 - -arcsin x = π / 2 + π / 2 - arccos x
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case hg
α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f₁ f₂ : α → K
g : α → R
t : R
l : Filter α
hmul : Tendsto (fun x ↦ f₁ x • g x) l (𝓝 t)
hf₁ : Tendsto f₁ l (cobounded K)
hbdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f₁ x - f₂ x‖
⊢ Tendsto (fun x ↦ ‖g x‖) l (𝓝 0)

Tactic:
· rw [← tendsto_zero_iff_norm_tendsto_zero]
    exact tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded hmul.norm.isBoundedUnder_le hf₁

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

Goal state before:
pp: case hbdd
R : Type u_4
K : Type u_5
inst✝¹⁰ : NormedRing K
inst✝⁹ : IsDomain K
inst✝⁸ : NormedAddCommGroup R
inst✝⁷ : Module K R
inst✝⁶ : IsTorsionFree K R
inst✝⁵ : NormSMulClass K R
inst✝⁴ : NormSMulClass ℤ K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorSemiring K
inst✝ : HasSolidNorm K
g : ℕ → R
t : R
hg : Tendsto (fun n ↦ ↑n • g n) atTop (𝓝 t)
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖↑⌊x⌋₊ - x‖

Tactic:
apply isBoundedUnder_of_eventually_le (a := ‖(1 : K)‖)

Goal state after:
case hbdd
R : Type u_4
K : Type u_5
inst✝¹⁰ : NormedRing K
inst✝⁹ : IsDomain K
inst✝⁸ : NormedAddCommGroup R
inst✝⁷ : Module K R
inst✝⁶ : IsTorsionFree K R
inst✝⁵ : NormSMulClass K R
inst✝⁴ : NormSMulClass ℤ K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorSemiring K
inst✝ : HasSolidNorm K
g : ℕ → R
t : R
hg : Tendsto (fun n ↦ ↑n • g n) atTop (𝓝 t)
⊢ ∀ᶠ (x : K) in atTop, ‖↑⌊x⌋₊ - x‖ ≤ ‖1‖
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case mp.inl
x : ℝ
h : log x = 0
x_lt_zero : x < 0
⊢ x = 0 ∨ x = 1 ∨ x = -1

Tactic:
refine Or.inr (Or.inr (neg_eq_iff_eq_neg.mp ?_))

Goal state after:
case mp.inl
x : ℝ
h : log x = 0
x_lt_zero : x < 0
⊢ -x = 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case succ.inr
x : ℝ
n : ℕ
ih : log (x ^ n) = ↑n * log x
hx : x ≠ 0
⊢ log (x ^ (n + 1)) = ↑(n + 1) * log x

Tactic:
rw [pow_succ, log_mul (pow_ne_zero _ hx) hx, ih, Nat.cast_succ, add_mul, one_mul]

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

Goal state before:
pp: θ : ℝ
⊢ ↑(2 • (θ / 2)) = ↑θ

Tactic:
two_nsmul,

Goal state after:
θ : ℝ
⊢ ↑(θ / 2 + θ / 2) = ↑θ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ - ↑π = θ + ↑π

Tactic:
rw [sub_eq_add_neg, neg_coe_pi]

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

Goal state before:
pp: θ : Angle
⊢ ↑π = ↑(2 • (π / 2))

Tactic:
two_nsmul,

Goal state after:
θ : Angle
⊢ ↑π = ↑(π / 2 + π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case refine_1
s : Set ℂ
hs : (cexp ⁻¹' s).Countable
⊢ s ⊆ insert 0 (cexp '' cexp ⁻¹' s)

Tactic:
rw [Set.image_preimage_eq_inter_range, range_exp, ← Set.sdiff_eq, ← Set.union_singleton,
        Set.sdiff_union_self]

Goal state after:
case refine_1
s : Set ℂ
hs : (cexp ⁻¹' s).Countable
⊢ s ⊆ s ∪ {0}
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: s : Set ℂ
⊢ (cexp ⁻¹' s).Countable ↔ s.Countable

Tactic:
by
  refine ⟨fun hs => ?_, fun hs => ?_⟩
  · refine ((hs.image exp).insert 0).mono ?_
    rw [Set.image_preimage_eq_inter_range, range_exp, ← Set.sdiff_eq, ← Set.union_singleton,
        Set.sdiff_union_self]
    exact Set.subset_union_left
  · rw [← Set.biUnion_preimage_singleton]
    refine hs.biUnion fun z hz => ?_
    by_cases! h : ∃ w, exp w = z
    · rcases h with ⟨w, rfl⟩
      simp only [Set.preimage, Set.mem_singleton_iff, exp_eq_exp_iff_exists_int, Set.ofPred_exists]
      exact Set.countable_iUnion fun m => Set.countable_singleton _
    · simp [Set.preimage, h]

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

Goal state before:
pp: case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
⊢ ↑θ = ↑ψ

Tactic:
obtain ⟨n, hn⟩ : ∃ n, n • _ = _ := QuotientAddGroup.leftRel_apply.mp (Quotient.exact' hc)

Goal state after:
case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑π = 0
hs : ↑θ + ↑ψ = ↑π
n : ℤ
hn : n • (2 * π) = -π + 0
⊢ ↑θ = ↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (↑(2 • θ.toReal)).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal

Tactic:
two_nsmul,

Goal state after:
θ : Angle
⊢ (↑(θ.toReal + θ.toReal)).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (↑(2 • θ.toReal)).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2

Tactic:
two_nsmul,

Goal state after:
θ : Angle
⊢ (↑(θ.toReal + θ.toReal)).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h.h
x✝¹ x✝ : ℝ
h : ↑(2 • (x✝¹ + x✝)) = ↑π
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹

Tactic:
two_nsmul,

Goal state after:
case h.h
x✝¹ x✝ : ℝ
h : ↑(x✝¹ + x✝ + (x✝¹ + x✝)) = ↑π
⊢ (↑x✝).tan = (↑x✝¹).tan⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ (↑(π / 2)).sign = 1

Tactic:
rw [sign, sin_coe, sin_pi_div_two, sign_one]

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

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
⊢ x ^ y = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
by
  simp only [rpow_def_of_nonneg hx]
  split_ifs <;> simp [*, exp_ne_zero]

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 (pure 0)

Tactic:
tendsto_pure

Goal state after:
hb₀ : -1 < 0
hb₁ : 0 < 1
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ^ x = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: case hdb
s : ℝ
n : ℕ
hn : s < ↑n
x : ℝ
hx₀ : 0 < x
hx₁ : 1 ≤ x
⊢ x ^ s ≤ x ^ n

Tactic:
simpa using rpow_le_rpow_of_exponent_le hx₁ hn.le

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

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

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

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

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℂ
⊢ ‖↑n ^ s‖ = ↑n ^ s.re

Tactic:
by
  rw [← ofReal_natCast, norm_cpow_eq_rpow_re_of_pos (Nat.cast_pos.mpr hn) _]

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

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x ^ z⁻¹ ≤ y ↔ y ^ z ≤ x

Tactic:
rw [← rpow_le_rpow_iff_of_neg hy _ hz, rpow_inv_rpow _ hz.ne]

Goal state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 ≤ x

x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ 0 < x ^ z⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case pos.inr
x : ℝ≥0
y : ℝ
h : 0 ≤ y
hx : x = 0
H : 0 < y
⊢ ↑(x ^ y) = ↑x ^ y

Tactic:
· simp [hx, zero_rpow_of_pos H, NNReal.zero_rpow (ne_of_gt H)]

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

Goal state before:
pp: case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ y = 0 ↔ ↑x = 0 ∧ 0 < y ∨ ↑x = ∞ ∧ y < 0

Tactic:
simp [← coe_rpow_of_ne_zero h, h]

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

Goal state before:
pp: case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ y = ∞ ↔ ↑x = 0 ∧ y < 0 ∨ ↑x = ∞ ∧ 0 < y

Tactic:
simp [← coe_rpow_of_ne_zero h, h]

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

Goal state before:
pp: x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < (y - 1 + 1) ^ m
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y

Tactic:
rw [tsub_add_cancel_of_le hy.le] at hm

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

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

Tactic:
← rpow_one x

Goal state after:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ 1 ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

Tactic:
← rpow_one x

Goal state after:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ 1 < y ^ z⁻¹ ↔ x ^ z < y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
⊢ √(‖x‖ * ((1 + 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:
← mul_div_assoc,

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.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
hx : 0 ≤ x.im
⊢ √(‖x‖ * ((1 - 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:
← mul_div_assoc,

Goal state after:
x : ℂ
hx : 0 ≤ x.im
⊢ √(‖x‖ * (1 - Real.cos x.arg) / 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‖ * ((1 - 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:
← mul_div_assoc,

Goal state after:
x : ℂ
hx : x.im < 0
⊢ -√(‖x‖ * (1 - Real.cos x.arg) / 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‖ * ((1 - Real.cos x.arg) / 2)) = √((‖x‖ - x.re) / 2)

Tactic:
← mul_div_assoc,

Goal state after:
x : ℂ
⊢ √(‖x‖ * (1 - Real.cos x.arg) / 2) = √((‖x‖ - x.re) / 2)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ ↑m ^ b = ↑r

Tactic:
hb.to_eq rfl rfl,

Goal state after:
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ ↑m ^ (↑n / ↑d) = ↑r
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ ↑m ^ b = ↑r

Tactic:
hb.to_eq rfl rfl,

Goal state after:
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ ↑m ^ (↑n / ↑d) = ↑r
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
⊢ midpoint R p₂ p₁ -ᵥ p₂ = ⅟2 • (p₁ -ᵥ p₂)

Tactic:
midpoint_vsub_left

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
⊢ ⅟2 • (p₁ -ᵥ p₂) = ⅟2 • (p₁ -ᵥ p₂)
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_1.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
r₁ r₂ : R
hr₁ : 0 < r₁
left✝ : 0 < r₂
h : r₁ • x = r₂ • y
⊢ ∑ i, ![r₁, -r₂] i • ![x, y] i = 0 ∧ ∃ i, ![r₁, -r₂] i ≠ 0

Tactic:
Fin.sum_univ_two,

Goal state after:
case neg.refine_1.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
r₁ r₂ : R
hr₁ : 0 < r₁
left✝ : 0 < r₂
h : r₁ • x = r₂ • y
⊢ ![r₁, -r₂] 0 • ![x, y] 0 + ![r₁, -r₂] 1 • ![x, y] 1 = 0 ∧ ∃ i, ![r₁, -r₂] i ≠ 0
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_1.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
r₁ r₂ : R
hr₁ : 0 < r₁
left✝ : 0 < r₂
h : r₁ • x = r₂ • -y
⊢ ∑ i, ![r₁, r₂] i • ![x, y] i = 0 ∧ ∃ i, ![r₁, r₂] i ≠ 0

Tactic:
Fin.sum_univ_two,

Goal state after:
case neg.refine_1.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
r₁ r₂ : R
hr₁ : 0 < r₁
left✝ : 0 < r₂
h : r₁ • x = r₂ • -y
⊢ ![r₁, r₂] 0 • ![x, y] 0 + ![r₁, r₂] 1 • ![x, y] 1 = 0 ∧ ∃ i, ![r₁, r₂] i ≠ 0
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_2
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : ∑ i, m i • ![x, y] i = 0
hmne : ∃ i, m i ≠ 0
⊢ SameRay R x y ∨ SameRay R x (-y)

Tactic:
Fin.sum_univ_two,

Goal state after:
case neg.refine_2
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • ![x, y] 0 + m 1 • ![x, y] 1 = 0
hmne : ∃ i, m i ≠ 0
⊢ SameRay R x y ∨ SameRay R x (-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
p : P1
v : V1
c : k
⊢ (lineMap p (v +ᵥ p)) c = c • v +ᵥ p

Tactic:
rw [lineMap_apply, vadd_vsub]

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

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V₁
inst✝² : Module k V₁
inst✝¹ : AffineSpace V₁ P₁
inst✝ : Invertible 2
x y : V₁
h : 2 • x = 2 • y
⊢ x = y

Tactic:
two_nsmul,

Goal state after:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V₁
inst✝² : Module k V₁
inst✝¹ : AffineSpace V₁ P₁
inst✝ : Invertible 2
x y : V₁
h : x + x = 2 • y
⊢ x = y
Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V₁
inst✝² : Module k V₁
inst✝¹ : AffineSpace V₁ P₁
inst✝ : Invertible 2
x y : V₁
h : x + x = 2 • y
⊢ x = y

Tactic:
two_nsmul,

Goal state after:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V₁
inst✝² : Module k V₁
inst✝¹ : AffineSpace V₁ P₁
inst✝ : Invertible 2
x y : V₁
h : x + x = y + y
⊢ x = 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
s : AffineSubspace k P
p : P
hp : p ∈ s
v : V
⊢ (∃ x ∈ ↑s, x -ᵥ p = -v) ↔ 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) ↔ ∃ x ∈ ↑s, p -ᵥ x = v
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 ↔ ∃ p₂ ∈ s, v = p -ᵥ p₂

Tactic:
rw [← SetLike.mem_coe, coe_direction_eq_vsub_set_left hp]
  exact ⟨fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩, fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩⟩

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
hb' : 0 < b
⊢ a * x + b * y ∈ Ico x y

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

Goal state after: