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

Goal state before:
pp: r : ℝ
⊢ ↑(ℜ ↑r) = ↑r

Tactic:
rw [realPart_apply_coe, star_def, conj_ofReal, ← two_smul ℝ (r : ℂ)]
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: r : ℝ
⊢ ↑(ℑ ↑r) = ↑0

Tactic:
simp [imaginaryPart_apply_coe, conj_ofReal]

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
h₂ : (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k
⊢ ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k

Tactic:
← sum_add_distrib

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
h₂ : (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k
⊢ ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ x ∈ range K, (f x * (∑ k ∈ range (K - x), g k - ∑ k ∈ range K, g k) + f x * ∑ k ∈ range K, g k)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝² : NormedAddCommGroup E''
inst✝¹ : NormedAddCommGroup F''
l : Filter α
inst✝ : l.NeBot
d : E''
c : F''
this : ¬Tendsto (Function.const α ‖c‖) l atTop
⊢ ((fun _x ↦ d) =o[l] fun _x ↦ c) ↔ d = 0

Tactic:
simp only [isLittleO_const_left, or_iff_left_iff_imp]

Goal state after:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝² : NormedAddCommGroup E''
inst✝¹ : NormedAddCommGroup F''
l : Filter α
inst✝ : l.NeBot
d : E''
c : F''
this : ¬Tendsto (Function.const α ‖c‖) l atTop
⊢ Tendsto (norm ∘ fun _x ↦ c) l atTop → d = 0
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
h : I * sin (x * I) = -sinh x
⊢ sin (x * I) = sinh x * I

Tactic:
← neg_neg (sinh x),

Goal state after:
x : ℂ
h : I * sin (x * I) = -sinh x
⊢ sin (x * I) = - -sinh x * I
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
ha : a ≠ 0
⊢ f =O[l] g

Tactic:
by
  obtain ⟨C, hC, ha⟩ : ∃ C, 0 < C ∧ C⁻¹ < ‖a‖ := ⟨‖a‖⁻¹ + 1, by positivity, by field_simp; simpa⟩
  simp only [IsBigO]
  exact ⟨C, isBigOWith_of_div_tendsto_nhds h hC ha⟩

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

Goal state before:
pp: x : ℝ
⊢ cosh x ^ 2 = sinh x ^ 2 + 1

Tactic:
by rw [← ofReal_inj]; simp [cosh_sq]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : OpenPartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
C : ℝ
h : IsBigOWith C (𝓝 b) f g
⊢ Tendsto (↑e) (𝓝 (↑e.symm b)) (𝓝 b)

Tactic:
have := e.continuousAt (e.map_target hb)

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : OpenPartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
C : ℝ
h : IsBigOWith C (𝓝 b) f g
this : ContinuousAt (↑e) (↑e.symm b)
⊢ Tendsto (↑e) (𝓝 (↑e.symm b)) (𝓝 b)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 : (∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_2_to_1 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x
a : ℝ
ha : a ∈ Set.Ioo (-R) R
H : f =O[atTop] fun x ↦ a ^ x
b : ℝ
hab : |a| < b
hbR : b < R
⊢ ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x

Tactic:
exact ⟨b, ⟨(abs_nonneg a).trans_lt hab, hbR⟩,
      H.trans_isLittleO (isLittleO_pow_pow_of_abs_lt_left (hab.trans_le (le_abs_self b)))⟩

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

Goal state before:
pp: case inr
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 : (∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_2_to_1 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x
tfae_3_to_2 : (∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x
tfae_2_to_4 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x
tfae_4_to_3 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_4_to_6 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n) →
    ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
a : ℝ
ha : a < R
C : ℝ
h₀ : 0 < C ∨ 0 < R
H : ∀ (n : ℕ), |f n| ≤ C * a ^ n
hC₀ : 0 < C
ha₀ : 0 ≤ a
⊢ ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x

Tactic:
exact ⟨a, A ⟨ha₀, ha⟩,
      isBigO_of_le' _ fun n ↦ (H n).trans <| mul_le_mul_of_nonneg_left (le_abs_self _) hC₀.le⟩

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

Goal state before:
pp: ⊢ comap rexp (𝓝[>] 0) = atBot

Tactic:
rw [← map_exp_atBot, comap_map exp_injective]

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

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

Tactic:
by
  rw [← smul_ball_one, mul_smul_comm, mul_ball_one]

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

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

Tactic:
have A : (1 : ℝ) < 2 ^ (n + 1) := one_lt_pow₀ one_lt_two n.succ_ne_zero

Goal state after:
n : ℕ
A : 1 < 2 ^ (n + 1)
⊢ cos (π / 2 ^ (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2
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
c : 𝕜
hc : c ≠ 0
⊢ ball (c • 0) (‖c‖ * 1) = ball 0 ‖c‖

Tactic:
smul_zero,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
⊢ ball 0 (‖c‖ * 1) = ball 0 ‖c‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ tan (π / 6) = 1 / √3

Tactic:
by
  rw [tan_eq_sin_div_cos, sin_pi_div_six, cos_pi_div_six]
  ring

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

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set E
x : E
⊢ infEDist x s ≤ ENNReal.ofReal (ε + δ) → infEDist x (cthickening δ s) ≤ ENNReal.ofReal ε

Tactic:
ENNReal.ofReal_add hε hδ,

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set E
x : E
⊢ infEDist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ → infEDist x (cthickening δ s) ≤ ENNReal.ofReal ε
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
⊢ closedBall (c • 0) (‖c‖ * 1) = closedBall 0 ‖c‖

Tactic:
smul_zero,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
⊢ closedBall 0 (‖c‖ * 1) = closedBall 0 ‖c‖
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 fun n ↦ f (n + N)

Tactic:
refine .of_norm_bounded (g := fun n ↦ ‖f N‖ * r ^ n)
      (Summable.mul_left _ <| summable_geometric_of_lt_one hr₀ hr₁) fun 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‖
n : ℕ
⊢ ‖f (n + N)‖ ≤ ‖f N‖ * r ^ n
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
hUV : (U ∩ V).Nonempty
⊢ IsPathConnected (U ∪ V)

Tactic:
rcases hUV with ⟨x, xU, xV⟩

Goal state after:
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
⊢ IsPathConnected (U ∪ V)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : 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 * w ^ n‖ ≤ C
⊢ CauchySeq fun s ↦ ∑ b ∈ s, f b * z ^ b

Tactic:
refine cauchySeq_finset_of_geometric_bound (r := ‖z‖ / ‖w‖) (C := C) ((div_lt_one hw).mpr hz)
    (fun n ↦ ?_)

Goal state after:
α : 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 * w ^ n‖ ≤ C
n : ℕ
⊢ ‖f n * z ^ n‖ ≤ C * (‖z‖ / ‖w‖) ^ n
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case inr
x y : ℝ
h : log x < y
hx : 0 < x
⊢ x < rexp y

Tactic:
· exact (log_lt_iff_lt_exp hx).mp h

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

Goal state before:
pp: ψ θ : Angle
this : Int.natAbs 2 = 2
⊢ (∃ k, ψ = θ + ↑k • ↑(2 * π / ↑2)) ↔ ψ = θ ∨ ψ = θ + ↑π

Tactic:
Fin.exists_fin_two,

Goal state after:
ψ θ : Angle
this : Int.natAbs 2 = 2
⊢ ψ = θ + ↑0 • ↑(2 * π / ↑2) ∨ ψ = θ + ↑1 • ↑(2 * π / ↑2) ↔ ψ = θ ∨ ψ = θ + ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hθ : |θ.toReal| < π / 2
hψ : |ψ.toReal| < π / 2
⊢ 2 • θ = 2 • ψ ↔ θ = ψ

Tactic:
two_nsmul_eq_iff_eq_of_abs_toReal_lt_pi_div_two hθ hψ

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

Goal state before:
pp: x y : ℂ
⊢ ↑x.arg = ↑y.arg ↔ x.arg = y.arg

Tactic:
simp_rw [← Real.Angle.toReal_inj, arg_coe_angle_toReal_eq_arg]

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

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

Tactic:
rw [sub_eq_iff_eq_add, ← mul_inv_cancel_left₀ two_ne_zero π, mul_assoc, ← mul_add,
    mul_right_inj' (two_ne_zero' ℝ), ← eq_sub_iff_add_eq', mul_inv_cancel_left₀ two_ne_zero π,
    inv_mul_eq_div, mul_comm] at h

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

Goal state before:
pp: case inr
θ ψ : Angle
hθs : θ.toReal ∈ Set.Ioo 0 π
hψs : ψ.toReal ∈ Set.Ioo 0 π
hsa : (θ + ψ).sign ≠ 1
this : ↑(θ + ψ).toReal = ↑(θ.toReal + ψ.toReal)
k : ℤ
hk : (θ + ψ).toReal - (θ.toReal + ψ.toReal) = 2 * π * ↑k
h : θ + ψ = ↑π
⊢ |(θ + ψ).toReal| = 2 * π - (|θ.toReal| + |ψ.toReal|)

Tactic:
simp_all only [sign_coe_pi, ne_eq, zero_ne_one, not_false_eq_true, toReal_pi, coe_add,
      coe_toReal, pi_pos, abs_of_pos]
    obtain rfl : k = 0 := IsStrictOrderedRing.int_eq_of_mul_mem_Ioo two_pi_pos (by grind)
    grind

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

Goal state before:
pp: case inl
x q : ℝ
h : x ≠ 0 ∨ 0 < q
⊢ ContinuousAt (fun x ↦ x ^ q) x

pp: case inr
x : ℝ
⊢ ContinuousAt (fun x ↦ x ^ 0) x

Tactic:
· exact (continuousAt_rpow (x, q) h).comp₂ continuousAt_id continuousAt_const

Goal state after:
case inr
x : ℝ
⊢ ContinuousAt (fun x ↦ x ^ 0) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: y : ℝ
hy : 0 < y
⊢ (orderIsoRpow y hy).symm = orderIsoRpow (1 / y) ⋯

Tactic:
simp only [orderIsoRpow, one_div_one_div]; rfl

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

Goal state before:
pp: x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
⊢ x ^ y ≤ x ^ z ↔ z ≤ y

Tactic:
← log_le_log_iff (rpow_pos_of_pos hx0 y) (rpow_pos_of_pos hx0 z),

Goal state after:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
⊢ log (x ^ y) ≤ log (x ^ z) ↔ z ≤ y
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 ↔ x = y ^ z

Tactic:
← rpow_left_inj _ hy hz,

Goal state after:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : z ≠ 0
⊢ (x ^ z⁻¹) ^ z = y ^ z ↔ x = y ^ z

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 inl
y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hxy : 0 ≤ y
⊢ (0 * y) ^ z = if (0 = 0 ∧ y = ∞ ∨ 0 = ∞ ∧ y = 0) ∧ z < 0 then ∞ else 0 ^ z * y ^ z

Tactic:
induction y <;> rcases hz with hz | hz

Goal state after:
case inl.top.inl
z : ℝ
hxy : 0 ≤ ∞
hz : z < 0
⊢ (0 * ∞) ^ z = if (0 = 0 ∧ ∞ = ∞ ∨ 0 = ∞ ∧ ∞ = 0) ∧ z < 0 then ∞ else 0 ^ z * ∞ ^ z

case inl.top.inr
z : ℝ
hxy : 0 ≤ ∞
hz : 0 < z
⊢ (0 * ∞) ^ z = if (0 = 0 ∧ ∞ = ∞ ∨ 0 = ∞ ∧ ∞ = 0) ∧ z < 0 then ∞ else 0 ^ z * ∞ ^ z

case inl.coe.inl
z : ℝ
x✝ : ℝ≥0
hxy : 0 ≤ ↑x✝
hz : z < 0
⊢ (0 * ↑x✝) ^ z = if (0 = 0 ∧ ↑x✝ = ∞ ∨ 0 = ∞ ∧ ↑x✝ = 0) ∧ z < 0 then ∞ else 0 ^ z * ↑x✝ ^ z

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

Goal state before:
pp: case inl
y : ℝ≥0∞
z : ℝ
hz : z < 0 ∨ 0 < z
hxy : 0 ≤ y
⊢ (0 * y) ^ z = if (0 = 0 ∧ y = ∞ ∨ 0 = ∞ ∧ y = 0) ∧ z < 0 then ∞ else 0 ^ z * y ^ z

Tactic:
induction y <;> rcases hz with hz | hz <;> simp [*, hz.not_gt]

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

Goal state before:
pp: case inr.inr
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
⊢ ContinuousAt (fun a ↦ a ^ y) x

Tactic:
have z_pos : 0 < z := by simpa [hz] using hy

Goal state after:
case inr.inr
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
z_pos : 0 < z
⊢ ContinuousAt (fun a ↦ a ^ y) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
s : ℂ
hs : 1 < s.re
⊢ 1 - ↑p ^ (-s) ≠ 0

Tactic:
by
  refine sub_ne_zero_of_ne fun H ↦ ?_
  have := norm_prime_cpow_le_one_half ⟨p, hp⟩ hs
  simp only at this
  rw [← H, norm_one] at this
  norm_num at this

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

Goal state before:
pp: x : ℝ
⊢ √x = x ^ (1 / 2)

Tactic:
obtain h | h := le_or_gt 0 x

Goal state after:
case inl
x : ℝ
h : 0 ≤ x
⊢ √x = x ^ (1 / 2)

case inr
x : ℝ
h : x < 0
⊢ √x = x ^ (1 / 2)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
z : ℝ
⊢ x.toReal ^ z = (x ^ z).toReal

Tactic:
ENNReal.toReal,

Goal state after:
x : ℝ≥0∞
z : ℝ
⊢ ↑x.toNNReal ^ z = (x ^ z).toReal
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
z : ℝ
⊢ ↑x.toNNReal ^ z = (x ^ z).toReal

Tactic:
ENNReal.toReal,

Goal state after:
x : ℝ≥0∞
z : ℝ
⊢ ↑x.toNNReal ^ z = ↑(x ^ z).toNNReal
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
x y : P
⊢ (2 * ⅟2) • (y -ᵥ x) +ᵥ x = y

Tactic:
mul_invOf_self,

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
x y : P
⊢ 1 • (y -ᵥ x) +ᵥ x = y
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
x y : P
⊢ midpoint R x y = midpoint R y x

Tactic:
rw [midpoint, ← lineMap_apply_one_sub, one_sub_invOf_two, midpoint]

Goal state after:
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
⊢ (2 * ⅟2) • (x + y) - x = y

Tactic:
mul_invOf_self,

Goal state after:
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ 1 • (x + y) - x = y
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_2.inl.inr.inl
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
hx : ¬x = 0
hy : ¬y = 0
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : m 0 < 0
hm1 : m 1 = 0
⊢ False

Tactic:
simp [hm1, hx, hm0.ne] at hm

Goal state after:
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
⊢ (∀ (p : P1) (x : ι), (fv x) p = 0 p x) ↔ ∀ (i : ι) (p : P1), (fv i) p = 0 p

Tactic:
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
inst✝ : ZeroLEOneClass 𝕜
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
⊢ {c} ⊆ [c -[𝕜] x] ∩ [c -[𝕜] y]

Tactic:
simp [singleton_subset_iff, left_mem_segment]

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

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ x ∈ [y -[𝕜] z] → ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x

pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ (∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x) → x ∈ [y -[𝕜] z]

Tactic:
· rintro ⟨a, b, ha, hb, hab, rfl⟩
    use a, b, ha, hb
    simp [*]

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ (∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x) → x ∈ [y -[𝕜] z]
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMulWithZero 𝕜 E
s : Set E
x : E
x✝ : x ∈ s
h : ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • 0 + b • x ∈ s

Tactic:
smul_zero,

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMulWithZero 𝕜 E
s : Set E
x : E
x✝ : x ∈ s
h : ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ 0 + b • x ∈ s
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 : x < y
⊢ z ∈ [x -[𝕜] y]

Tactic:
rw [← sub_pos] at h

Goal state after:
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]
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₂ p₁a : P
hp₁a : p₁a ∈ s
v₁ : V
hv₁ : v₁ ∈ vectorSpan k s
hv₁p : p₁ = v₁ +ᵥ p₁a
p₂a : P
hp₂a : p₂a ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hv₂p : p₂ = v₂ +ᵥ p₂a
hv₁v₂ : v₁ - v₂ ∈ vectorSpan k s
⊢ p₁a -ᵥ p₂a + (v₁ - v₂) ∈ vectorSpan k s

Tactic:
refine (vectorSpan k s).add_mem ?_ hv₁v₂

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₂ p₁a : P
hp₁a : p₁a ∈ s
v₁ : V
hv₁ : v₁ ∈ vectorSpan k s
hv₁p : p₁ = v₁ +ᵥ p₁a
p₂a : P
hp₂a : p₂a ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hv₂p : p₂ = v₂ +ᵥ p₂a
hv₁v₂ : v₁ - v₂ ∈ vectorSpan k s
⊢ p₁a -ᵥ p₂a ∈ vectorSpan k s
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 • x + bp • y) + b • (aq • x + bq • y) ∈ [x -[𝕜] y]

Tactic:
refine
    ⟨a * ap + b * aq, a * bp + b * bq, add_nonneg (mul_nonneg ha hap) (mul_nonneg hb haq),
      add_nonneg (mul_nonneg ha hbp) (mul_nonneg hb hbq), ?_, ?_⟩

Goal state after:
case refine_1
𝕜 : 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 + (a * bp + b * bq) = 1

case refine_2
𝕜 : 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) • x + (a * bp + b * bq) • y = a • (ap • x + bp • y) + b • (aq • x + bq • y)
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case refine_1.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
hz : a * x + b * y ∈ Ioc x y
hb' : 0 < b
⊢ ∃ a_1 b_1, 0 ≤ a_1 ∧ 0 < b_1 ∧ a_1 + b_1 = 1 ∧ a_1 * x + b_1 * y = a * x + b * y

Tactic:
exact ⟨a, b, ha, hb', hab, rfl⟩

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
h : 0 ∈ s
x : V
⊢ x ∈ ↑s.direction ↔ x ∈ s

Tactic:
rw [Submodule.mem_toAffineSubspace, ← SetLike.mem_coe]

Goal state after:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : AffineSubspace k V
h : 0 ∈ s
x : V
⊢ x ∈ ↑s.direction ↔ x ∈ s