mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h✝ : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec✝ :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
⊢ ∃ c, ∀ᶠ (x : ℕ) in atTop, ‖f x‖ ≤ c * ‖g x‖

Tactic:
rw [← eventually_forall_ge_atTop] at hrec

Goal state after:
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h✝ : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec✝ :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
⊢ ∃ c, ∀ᶠ (x : ℕ) in atTop, ‖f x‖ ≤ c * ‖g x‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : |x| ≤ 1
⊢ 0 < m

Tactic:
· lia

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
n : ℤ
hn : Odd n
⊢ a ^ n ≤ 0 ↔ a ≤ 0

Tactic:
by
  rw [le_iff_lt_or_eq, le_iff_lt_or_eq, hn.zpow_neg_iff, zpow_eq_zero_iff]
  rintro rfl
  exact Int.not_even_iff_odd.2 hn .zero

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

Goal state before:
pp: case hzero
f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
hrec : ∀ᶠ (n₀ : ℕ) in atTop, ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
⊢ ∀ᶠ (n : ℕ) in atTop, g n = 0 → f n = 0

pp: case hrec
f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
hrec : ∀ᶠ (n₀ : ℕ) in atTop, ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
⊢ ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖

Tactic:
case hzero => filter_upwards [hf, hg]; grind

Goal state after:
case hrec
f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
hrec : ∀ᶠ (n₀ : ℕ) in atTop, ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
⊢ ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) (cexp 0) < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
hxy : dist x y < δ
⊢ dist (x - y) 0 < δ

Tactic:
simpa only [dist_eq_norm, sub_zero] using hxy

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

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

Tactic:
have kn : k + n.succ ≥ n.succ := by
      rw [← zero_add n.succ]; exact add_le_add (Nat.zero_le _) (by simp)
    rw [hk, Nat.succ_add, pow_succ r, ← mul_assoc]
    refine
      le_trans (by rw [mul_comm] <;> exact h _ (Nat.le_of_succ_le kn))
        (mul_le_mul_of_nonneg_right ?_ hr0)
    exact ih _ h _ (by simp) rfl

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
a : M
this✝ : Nonempty ↑{m | ↑m = ↑a}
b : M
this : Nonempty ↑{m | ↑m = ↑b}
⊢ dist 1 ↑⟨a * b, ⋯⟩ ≤ dist 1 ↑⟨a, ⋯⟩ + dist 1 ↑⟨b, ⋯⟩

Tactic:
simpa using norm_mul_le' _ _

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : SeminormedAddCommGroup M
inst✝² : SeminormedAddCommGroup N
R : Type u_3
inst✝¹ : Ring R
inst✝ : Module R M
S : Submodule R M
__spread✝⁻⁰ : (M ⧸ S) ≃ₗ[R] M ⧸ S := S.quotEquivOfEq S ⋯
⊢ ∀ (x : M ⧸ S), ‖(S.quotEquivOfEq S ⋯) x‖ = ‖x‖

Tactic:
rintro ⟨_⟩

Goal state after:
case mk
M : Type u_1
N : Type u_2
inst✝³ : SeminormedAddCommGroup M
inst✝² : SeminormedAddCommGroup N
R : Type u_3
inst✝¹ : Ring R
inst✝ : Module R M
S : Submodule R M
__spread✝⁻⁰ : (M ⧸ S) ≃ₗ[R] M ⧸ S := S.quotEquivOfEq S ⋯
x✝ : M ⧸ S
a✝ : M
⊢ ‖(S.quotEquivOfEq S ⋯) (Quot.mk (⇑S.quotientRel) a✝)‖ = ‖Quot.mk (⇑S.quotientRel) a✝‖
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
⊢ ‖x‖⁻¹ • x ∈ closedBall 0 1

Tactic:
simp only [mem_closedBall_zero_iff, norm_smul, norm_inv, norm_norm, ← div_eq_inv_mul,
    div_self_le_one]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
⊢ ‖x‖⁻¹ • x ∈ closedBall 0 1

Tactic:
by
  simp only [mem_closedBall_zero_iff, norm_smul, norm_inv, norm_norm, ← div_eq_inv_mul,
    div_self_le_one]

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

Goal state before:
pp: R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n ↦ ↑(u n)) =O[atTop] fun n ↦ ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ (fun n ↦ ↑(n ^ k) * ‖r‖ ^ n) =O[atTop] fun n ↦ r' ^ n

Tactic:
simp only [cast_pow]

Goal state after:
R : Type u_4
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n ↦ ↑(u n)) =O[atTop] fun n ↦ ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ (fun n ↦ ↑n ^ k * ‖r‖ ^ n) =O[atTop] fun n ↦ r' ^ n
Module: Mathlib.Analysis.SpecificLimits.Normed

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

Tactic:
rcases h with ⟨N, hN⟩

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 f
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ₁ γ₂ : Path x y
h : γ₁.toContinuousMap = γ₂.toContinuousMap
⊢ γ₁ = γ₂

Tactic:
cases γ₁

Goal state after:
case mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ₂ : Path x y
toContinuousMap✝ : C(↑I, X)
source'✝ : toContinuousMap✝.toFun 0 = x
target'✝ : toContinuousMap✝.toFun 1 = y
h :
  { toContinuousMap := toContinuousMap✝, source' := source'✝, target' := target'✝ }.toContinuousMap = γ₂.toContinuousMap
⊢ { toContinuousMap := toContinuousMap✝, source' := source'✝, target' := target'✝ } = γ₂
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝ : PathConnectedSpace X
x : X
_x_in : x ∈ univ
hx : pathComponentIn univ x = univ
⊢ connectedComponent x = univ

Tactic:
← univ_subset_iff

Goal state after:
case h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝ y z : X
ι : Type u_3
F : Set X
inst✝ : PathConnectedSpace X
x : X
_x_in : x ∈ univ
hx : pathComponentIn univ x = univ
⊢ univ ⊆ connectedComponent x
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ mk x = mk y ↔ y ∈ pathComponent x

Tactic:
mem_pathComponent_iff

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ mk x = mk y ↔ Joined x y
Module: Mathlib.Analysis.Normed.Group.AddCircle

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

Tactic:
intro p hp hx

Goal state after:
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
⊢ ‖↑x‖ = |x|
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : 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 : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
⊢ Tendsto g l (𝓝 0)

Tactic:
obtain ⟨c, hc⟩ := hmul.eventually_le
  refine Metric.nhds_basis_closedBall.tendsto_right_iff.mpr fun ε hε0 ↦ ?_
  filter_upwards [hc, hasBasis_cobounded_norm.tendsto_right_iff.mp hf (c / ε) trivial,
    hf.eventually_ne_cobounded 0] with x hfgc hεf hf0
  rcases eq_or_lt_of_le ((norm_nonneg _).trans hfgc) with rfl | hc0
  · simpa [(smul_eq_zero_iff_right hf0).mp (norm_le_zero_iff.mp hfgc)] using hε0.le
  calc
    _ = ‖g x‖ := by simp
    _ ≤ c / ‖f x‖ := by rwa [norm_smul, ← le_div_iff₀' (by positivity)] at hfgc
    _ ≤ c / (c / ε) := by gcongr
    _ = ε := div_div_cancel₀ hc0.ne'

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

Goal state before:
pp: x : ℂ
hx : x ≠ 0
⊢ cexp (log x) = x

Tactic:
rw [log, exp_add_mul_I, ← ofReal_sin, sin_arg, ← ofReal_cos, cos_arg hx, ← ofReal_exp,
    Real.exp_log (norm_pos_iff.mpr hx), mul_add, ofReal_div, ofReal_div,
    mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), ← mul_assoc,
    mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), re_add_im]

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

Goal state before:
pp: x y : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
hy₁ : -π < y.im
hy₂ : y.im ≤ π
hxy : cexp x = cexp y
⊢ log (cexp x) = y

Tactic:
← log_exp hy₁ hy₂,

Goal state after:
x y : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
hy₁ : -π < y.im
hy₂ : y.im ≤ π
hxy : cexp x = cexp y
⊢ log (cexp x) = log (cexp y)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case inr
n : ℕ
hn : n ≠ 0
⊢ log ↑n = n.factorization.sum fun p t ↦ log ↑(p ^ t)

Tactic:
rw [← Finsupp.log_prod, ← Nat.cast_finsuppProd, Nat.prod_factorization_pow_eq_self hn]

Goal state after:
case inr.hg
n : ℕ
hn : n ≠ 0
⊢ ∀ (a : ℕ), ↑(a ^ n.factorization a) = 0 → n.factorization a = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: case mpr.inl
x : ℂ
h : x ≠ 0
⊢ 0 ^ x = 0

Tactic:
exact zero_cpow h

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

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

Tactic:
div_eq_mul_inv

Goal state after:
x y z : ℂ
hx : x ≠ 0
⊢ x ^ y * (x ^ z)⁻¹ = x ^ y * (x ^ z)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mpr.inl
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * ↑k
⊢ sin θ = sin ψ

pp: case mpr.inr
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * ↑k
⊢ sin θ = sin ψ

Tactic:
· rw [← sub_eq_zero, sin_sub_sin, H, mul_assoc 2 π k, mul_div_cancel_left₀ _ (two_ne_zero' ℝ),
        mul_comm π _, sin_int_mul_pi, mul_zero, zero_mul]

Goal state after:
case mpr.inr
θ ψ : ℝ
k : ℤ
H : θ - (π - ψ) = 2 * π * ↑k
⊢ sin θ = sin ψ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: ⊢ cos 0 = 1

Tactic:
rw [← coe_zero, cos_coe, Real.cos_zero]

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

Goal state before:
pp: a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
⊢ ↑a ^ r * (↑b ^ r)⁻¹ = ↑a ^ r / ↑b ^ r

Tactic:
div_eq_mul_inv

Goal state after:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
⊢ ↑a ^ r * (↑b ^ r)⁻¹ = ↑a ^ r * (↑b ^ r)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
h : 0 < x.re ∨ x.im ≠ 0
h₀ : ‖x‖ ≠ 0
⊢ ContinuousAt arg x

Tactic:
← lt_or_lt_iff_ne

Goal state after:
x : ℂ
h : 0 < x.re ∨ x.im < 0 ∨ 0 < x.im
h₀ : ‖x‖ ≠ 0
⊢ ContinuousAt arg x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
by
  simp only [sign, sin_two_nsmul, nsmul_eq_mul, Nat.cast_ofNat, sign_mul, Nat.ofNat_pos, sign_pos,
    one_mul, mul_right_eq_self₀, _root_.sign_eq_zero_iff, sign_eq_one_iff, sin_eq_zero_iff,
    cos_pos_iff_abs_toReal_lt_pi_div_two]
  have : 0 < π / 2 := by positivity
  grind

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

Goal state before:
pp: x y : ℝ
hx_nonneg : 0 ≤ x
h_rpow_nonneg : 0 ≤ x ^ y
⊢ |x ^ y| = |x| ^ y

Tactic:
abs_eq_self.mpr hx_nonneg,

Goal state after:
x y : ℝ
hx_nonneg : 0 ≤ x
h_rpow_nonneg : 0 ≤ x ^ y
⊢ |x ^ y| = x ^ y
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
hθ : θ ≠ ↑π
hψ : ψ ≠ ↑π
hs : θ.sign ≠ ψ.sign ∨ θ.sign = (θ + ψ).sign
⊢ (θ + ψ).toReal = θ.toReal + ψ.toReal

Tactic:
by
  obtain (hs | hs) := hs
  · obtain (h | h | h) := ψ.sign.trichotomy <;> obtain (h | h | h) := θ.sign.trichotomy
    all_goals grind [add_comm, toReal_add_of_sign_pos_sign_neg, sign_eq_zero_iff]
  · rw [← neg_neg θ.sign, ← sign_neg] at hs
    have := toReal_add_of_sign_eq_neg_sign (.inr <| by simpa [neg_eq_iff_eq_neg]) hs.symm
    simpa [toReal_neg_eq_neg_toReal_iff.mpr, hθ, ← sub_eq_add_neg, eq_sub_iff_add_eq', eq_comm]

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

Goal state before:
pp: x : ℝ≥0
y z : ℝ
hx₀ : x ≠ 0
hx₁ : x ≠ 1
⊢ x ^ y = x ^ z ↔ y = z

Tactic:
rw [← pos_iff_ne_zero] at hx₀

Goal state after:
x : ℝ≥0
y z : ℝ
hx₀ : 0 < x
hx₁ : x ≠ 1
⊢ x ^ y = x ^ z ↔ y = z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ x ^ y ≤ x ^ z

Tactic:
by
  repeat' rw [rpow_def_of_pos (lt_of_lt_of_le zero_lt_one hx)]
  rw [exp_le_exp]; gcongr; exact log_nonneg hx

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

Goal state before:
pp: x : ℝ≥0∞
y z : ℝ
hx : x ≠ 0
h'x : x ≠ ∞
⊢ x ^ y * (x ^ z)⁻¹ = x ^ y / x ^ z

Tactic:
div_eq_mul_inv

Goal state after:
x : ℝ≥0∞
y z : ℝ
hx : x ≠ 0
h'x : x ≠ ∞
⊢ x ^ y * (x ^ z)⁻¹ = x ^ y * (x ^ z)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℝ≥0
r : ℝ
⊢ ∏ i ∈ s, ↑(f i) ^ r = ↑(∏ i ∈ s, f i) ^ r

Tactic:
induction s using Finset.induction with

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

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

Tactic:
induction s using Finset.induction with

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

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

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert i s hi ih =>
    have h2f : ∀ i ∈ s, f i ≠ ∞ := fun i hi ↦ hf i <| mem_insert_of_mem hi
    rw [prod_insert hi, prod_insert hi, ih h2f, ← mul_rpow_of_ne_top <| hf i <| mem_insert_self ..]
    apply prod_ne_top h2f

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℝ≥0∞
r : ℝ
hr : 0 ≤ r
⊢ ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r

Tactic:
induction s using Finset.induction with

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

Goal state before:
pp: x y : ℝ≥0∞
z : ℝ
hz : 0 ≤ z
⊢ x ^ z * (y ^ z)⁻¹ = x ^ z / y ^ z

Tactic:
div_eq_mul_inv

Goal state after:
x y : ℝ≥0∞
z : ℝ
hz : 0 ≤ z
⊢ x ^ z * (y ^ z)⁻¹ = x ^ z * (y ^ z)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℂ
⊢ (x ^ ↑2⁻¹).re = √((‖x‖ + x.re) / 2)

Tactic:
cpow_ofReal_re,

Goal state after:
x : ℂ
⊢ ‖x‖ ^ 2⁻¹ * Real.cos (x.arg * 2⁻¹) = √((‖x‖ + x.re) / 2)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x p : ℝ
hx_pos : 0 < x
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
ENNReal.ofReal

Goal state after:
x p : ℝ
hx_pos : 0 < x
⊢ ↑x.toNNReal ^ p = ↑(x ^ p).toNNReal
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ SameRay R (-x) (-y) ↔ SameRay R x y

Tactic:
by
  simp only [SameRay, neg_eq_zero, smul_neg, neg_inj]

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

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
x✝¹ x✝ : P1 →ᵃ[k] P2
f : P1 → P2
f_linear : V1 →ₗ[k] V2
f_add : ∀ (p : P1) (v : V1), f (v +ᵥ p) = f_linear v +ᵥ f p
g : P1 → P2
g_linear : V1 →ₗ[k] V2
g_add : ∀ (p : P1) (v : V1), g (v +ᵥ p) = g_linear v +ᵥ g p
h : f = g
p : P1
⊢ { toFun := f, linear := f_linear, map_vadd' := f_add } = { toFun := g, linear := g_linear, map_vadd' := g_add }

Tactic:
congr with v

Goal state after:
case e_linear
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
x✝¹ x✝ : P1 →ᵃ[k] P2
f : P1 → P2
f_linear : V1 →ₗ[k] V2
f_add : ∀ (p : P1) (v : V1), f (v +ᵥ p) = f_linear v +ᵥ f p
g : P1 → P2
g_linear : V1 →ₗ[k] V2
g_add : ∀ (p : P1) (v : V1), g (v +ᵥ p) = g_linear v +ᵥ g p
h : f = g
p : P1
v : V1
⊢ f_linear v = g_linear v
Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹² : Ring k
inst✝¹¹ : AddCommGroup V₁
inst✝¹⁰ : AddCommGroup V₂
inst✝⁹ : AddCommGroup V₃
inst✝⁸ : AddCommGroup V₄
inst✝⁷ : Module k V₁
inst✝⁶ : Module k V₂
inst✝⁵ : Module k V₃
inst✝⁴ : Module k V₄
inst✝³ : AffineSpace V₁ P₁
inst✝² : AffineSpace V₂ P₂
inst✝¹ : AffineSpace V₃ P₃
inst✝ : AffineSpace V₄ P₄
e : P₁ → P₂
e' : V₁ ≃ₗ[k] V₂
p : P₁
h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p
p' : P₁
⊢ (fun q' ↦ e'.symm (q' -ᵥ e p) +ᵥ p) (e p') = p'

Tactic:
by simp [h p', vadd_vsub, vsub_vadd]

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
x y : M
⊢ SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]

Tactic:
by
  by_cases hx : x = 0; · simpa [hx] using fun h : LinearIndependent R ![0, y] => h.ne_zero 0 rfl
  by_cases hy : y = 0; · simpa [hy] using fun h : LinearIndependent R ![x, 0] => h.ne_zero 1 rfl
  simp_rw [Fintype.not_linearIndependent_iff]
  refine ⟨fun h => ?_, fun h => ?_⟩
  · rcases h with ((hx0 | hy0 | ⟨r₁, r₂, hr₁, _, h⟩) | (hx0 | hy0 | ⟨r₁, r₂, hr₁, _, h⟩))
    · exact False.elim (hx hx0)
    · exact False.elim (hy hy0)
    · refine ⟨![r₁, -r₂], ?_⟩
      rw [Fin.sum_univ_two, Fin.exists_fin_two]
      simp [h, hr₁.ne.symm]
    · exact False.elim (hx hx0)
    · exact False.elim (hy (neg_eq_zero.1 hy0))
    · refine ⟨![r₁, r₂], ?_⟩
      rw [Fin.sum_univ_two, Fin.exists_fin_two]
      simp [h, hr₁.ne.symm]
  · rcases h with ⟨m, hm, hmne⟩
    rw [Fin.sum_univ_two, add_eq_zero_iff_eq_neg] at hm
    dsimp only [Matrix.cons_val] at hm
    rcases lt_trichotomy (m 0) 0 with (hm0 | hm0 | hm0) <;>
      rcases lt_trichotomy (m 1) 0 with (hm1 | hm1 | hm1)
    · refine
        Or.inr (Or.inr (Or.inr ⟨-m 0, -m 1, Left.neg_pos_iff.2 hm0, Left.neg_pos_iff.2 hm1, ?_⟩))
      linear_combination (norm := module) -hm
    · exfalso
      simp [hm1, hx, hm0.ne] at hm
    · refine Or.inl (Or.inr (Or.inr ⟨-m 0, m 1, Left.neg_pos_iff.2 hm0, hm1, ?_⟩))
      linear_combination (norm := module) -hm
    · exfalso
      simp [hm0, hy, hm1.ne] at hm
    · rw [Fin.exists_fin_two] at hmne
      exact False.elim (not_and_or.2 hmne ⟨hm0, hm1⟩)
    · exfalso
      simp [hm0, hy, hm1.ne.symm] at hm
    · refine Or.inl (Or.inr (Or.inr ⟨m 0, -m 1, hm0, Left.neg_pos_iff.2 hm1, ?_⟩))
      rwa [neg_smul]
    · exfalso
      simp [hm1, hx, hm0.ne.symm] at hm
    · refine Or.inr (Or.inr (Or.inr ⟨m 0, m 1, hm0, hm1, ?_⟩))
      rwa [smul_neg]

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
h : ∀ ⦃y : E⦄, y ∈ s → [x -[𝕜] y] ⊆ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s

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

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
h : ∃ r, 0 < r ∧ r • x = y
⊢ SameRay R x y

Tactic:
rcases h with ⟨r, hr, rfl⟩

Goal state after:
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
hx : x ≠ 0
r : R
hr : 0 < r
hy : r • x ≠ 0
⊢ SameRay R x (r • x)
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
h : ∃ r, 0 ≤ r ∧ r • x = y
⊢ SameRay R x y

Tactic:
rcases h with ⟨r, hr, rfl⟩

Goal state after:
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
hx : x ≠ 0
r : R
hr : 0 ≤ r
⊢ SameRay R x (r • x)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
⊢ ⊤.direction = ⊤

Tactic:
by
  obtain ⟨p⟩ := S.nonempty
  ext v
  refine ⟨imp_intro Submodule.mem_top, fun _hv => ?_⟩
  have hpv : ((v +ᵥ p) -ᵥ p : V) ∈ (⊤ : AffineSubspace k P).direction :=
    vsub_mem_direction (mem_top k V _) (mem_top k V _)
  rwa [vadd_vsub] at hpv

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsBounded s
⊢ Bornology.IsVonNBounded 𝕜 s

Tactic:
by
  rcases h.subset_ball 0 with ⟨r, hr⟩
  rw [Metric.nhds_basis_ball.isVonNBounded_iff]
  rw [← ball_normSeminorm 𝕜 E] at hr ⊢
  exact fun ε hε ↦ ((normSeminorm 𝕜 E).ball_zero_absorbs_ball_zero hε).mono_right hr

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulMono 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ {x | x ∈ s ∧ f x ≤ r}
y : E
hy : y ∈ {x | x ∈ s ∧ f x ≤ r}
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ≤ a • r + b • r

Tactic:
gcongr
        · exact hx.2
        · exact hy.2

Goal state after: