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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (fun x ↦ f x * g x) =O[l] h ↔ g =O[l] fun x ↦ h x / f x

Tactic:
rw [isBigO_iff_isBigOWith, isBigO_iff_isBigOWith]

Goal state after:
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∃ c, IsBigOWith c l (fun x ↦ f x * g x) h) ↔ ∃ c, IsBigOWith c l g fun x ↦ h x / f x
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ
⊢ Tendsto (fun x ↦ rexp (f x)) l atTop ↔ Tendsto f l atTop

Tactic:
by
  simp_rw [← comp_apply (f := exp), ← tendsto_comap_iff, comap_exp_atTop]

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 T : Submodule R M
𝕜 : Type u_4
inst✝⁴ : SeminormedCommRing 𝕜
inst✝³ : Module 𝕜 M
inst✝² : IsBoundedSMul 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
k : 𝕜
x : M ⧸ S
ε : ℝ
hε : 0 < ε
⊢ ‖k • x‖ ≤ ‖k‖ * ‖x‖ + ε

Tactic:
have := (nhds_basis_ball.tendsto_iff nhds_basis_ball).mp
        ((@Real.uniformContinuous_const_mul ‖k‖).continuous.tendsto ‖x‖) ε hε

Goal state after:
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 T : Submodule R M
𝕜 : Type u_4
inst✝⁴ : SeminormedCommRing 𝕜
inst✝³ : Module 𝕜 M
inst✝² : IsBoundedSMul 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
k : 𝕜
x : M ⧸ S
ε : ℝ
hε : 0 < ε
this : ∃ ia, 0 < ia ∧ ∀ x_1 ∈ ball ‖x‖ ia, ‖k‖ * x_1 ∈ ball (‖k‖ * ‖x‖) ε
⊢ ‖k • x‖ ≤ ‖k‖ * ‖x‖ + ε
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
n : ℕ
⊢ x.sqrtTwoAddSeries (n + 1 + 1) = (√(2 + x)).sqrtTwoAddSeries (n + 1)

Tactic:
rw [sqrtTwoAddSeries, sqrtTwoAddSeries_succ _ _, sqrtTwoAddSeries]

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ s * closedBall 1 δ = cthickening δ s

Tactic:
by
  rw [hs.cthickening_eq_biUnion_closedBall hδ]
  ext x
  simp only [mem_mul, dist_eq_norm_div, exists_prop, mem_iUnion, mem_closedBall,
    ← eq_div_iff_mul_eq'', div_one, exists_eq_right]

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

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

Tactic:
by
  rw [cos_pi_div_six, div_pow, sq_sqrt] <;> norm_num

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

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

Tactic:
sin_pi_div_six,

Goal state after:
⊢ 1 / 2 / cos (π / 6) = 1 / √3
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
h0x : 0 < x
hxp : x < π / 2
⊢ 0 < sin x / cos x

Tactic:
exact div_pos (sin_pos_of_pos_of_lt_pi h0x (by linarith)) (cos_pos_of_mem_Ioo ⟨by linarith, hxp⟩)

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

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
P : ℕ[X] := (ascPochhammer ℕ k).comp (X + C 1)
n : ℕ
mP : P.Monic
dP : P.natDegree = k
A : (n + k).descFactorial k = Polynomial.eval n P
| Polynomial.eval n (X ^ P.natDegree + ∑ i ∈ Finset.range P.natDegree, C (P.coeff i) * X ^ i)

Tactic:
dP

Goal state after:
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
P : ℕ[X] := (ascPochhammer ℕ k).comp (X + C 1)
n : ℕ
mP : P.Monic
dP : P.natDegree = k
A : (n + k).descFactorial k = Polynomial.eval n P
| Polynomial.eval n (X ^ k + ∑ i ∈ Finset.range k, C (P.coeff i) * X ^ i)
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
F : Set X
h : x ∈ F
x✝¹ : X
x✝ : x✝¹ ∈ pathComponentIn F x
γ : Path x x✝¹
hγ : ∀ (t : ↑I), γ t ∈ F
⊢ JoinedIn (pathComponentIn F x) x x✝¹

Tactic:
by
    refine ⟨γ, fun t ↦
      ⟨(γ.truncateOfLE t.2.1).cast (γ.extend_zero.symm) (γ.extend_extends' t).symm, fun t' ↦ ?_⟩⟩
    dsimp [Path.truncateOfLE, Path.truncate]
    exact γ.extend_extends' ⟨min (max t'.1 0) t.1, by simp [t.2.1, t.2.2]⟩ ▸ hγ _

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

Goal state before:
pp: case neg
x : ℝ
h_zero : ¬x = 0
⊢ x ≤ rexp (log x)

Tactic:
rw [exp_log_eq_abs h_zero]

Goal state after:
case neg
x : ℝ
h_zero : ¬x = 0
⊢ x ≤ |x|
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
⊢ log |(-x)| = log |x|

Tactic:
abs_neg

Goal state after:
x : ℝ
⊢ log |x| = log |x|
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ 0 ≤ log x ↔ 1 ≤ x

Tactic:
by rw [← not_lt, log_neg_iff hx, not_lt]

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

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : |(-(log x * x))| < 1
aux : 0 ≤ -log x * x
⊢ |log x * x| < 1

Tactic:
abs_neg

Goal state after:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : |log x * x| < 1
aux : 0 ≤ -log x * x
⊢ |log x * x| < 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

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

Tactic:
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.Complex.Log

Goal state before:
pp: z : ℂ
⊢ cexp (log (cexp z)) = cexp z

Tactic:
exp_log

Goal state after:
z : ℂ
⊢ cexp z = cexp z

z : ℂ
⊢ cexp z ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: a : ℝ
ha : 0 < a
⊢ log '' Ioo 0 a = Iio (log a)

Tactic:
by
  nth_rw 1 [← exp_log ha, ← image_exp_Iio, ← image_comp, log_comp_exp, image_id]

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 : ↑θ + ↑ψ = ↑π
n : ℤ
hn : n • (2 * π) = -π + 0
⊢ ↑θ = ↑ψ

Tactic:
rw [← neg_one_mul, add_zero, ← sub_eq_zero, zsmul_eq_mul, ← mul_assoc, ← sub_mul, mul_eq_zero,
    eq_false (ne_of_gt pi_pos), or_false, sub_neg_eq_add, ← Int.cast_zero, ← Int.cast_one,
    ← Int.cast_ofNat, ← Int.cast_mul, ← Int.cast_add, Int.cast_inj] at hn

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

Goal state before:
pp: θ : Angle
ψ : ℝ
⊢ θ.cos = Real.cos ψ ↔ θ = ↑ψ ∨ θ = -↑ψ

Tactic:
induction θ using Real.Angle.induction_on

Goal state after:
case h
ψ x✝ : ℝ
⊢ (↑x✝).cos = Real.cos ψ ↔ ↑x✝ = ↑ψ ∨ ↑x✝ = -↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
ψ : ℝ
⊢ θ.sin = Real.sin ψ ↔ θ = ↑ψ ∨ θ + ↑ψ = ↑π

Tactic:
induction θ using Real.Angle.induction_on

Goal state after:
case h
ψ x✝ : ℝ
⊢ (↑x✝).sin = Real.sin ψ ↔ ↑x✝ = ↑ψ ∨ ↑x✝ + ↑ψ = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (-θ).sin = -θ.sin

Tactic:
induction θ using Real.Angle.induction_on

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

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

Tactic:
induction θ using Real.Angle.induction_on

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

Goal state before:
pp: θ : Angle
⊢ (-θ).cos = θ.cos

Tactic:
induction θ using Real.Angle.induction_on

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

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

Tactic:
induction θ using Real.Angle.induction_on

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

Goal state before:
pp: θ : Angle
⊢ θ.cos ^ 2 + θ.sin ^ 2 = 1

Tactic:
induction θ using Real.Angle.induction_on

Goal state after:
case h
x✝ : ℝ
⊢ (↑x✝).cos ^ 2 + (↑x✝).sin ^ 2 = 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (θ + ↑(π / 2)).sin = θ.cos

Tactic:
induction θ using Real.Angle.induction_on

Goal state after:
case h
x✝ : ℝ
⊢ (↑x✝ + ↑(π / 2)).sin = (↑x✝).cos
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (θ - ↑(π / 2)).sin = -θ.cos

Tactic:
induction θ using Real.Angle.induction_on

Goal state after:
case h
x✝ : ℝ
⊢ (↑x✝ - ↑(π / 2)).sin = -(↑x✝).cos
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (↑(π / 2) - θ).sin = θ.cos

Tactic:
induction θ using Real.Angle.induction_on

Goal state after:
case h
x✝ : ℝ
⊢ (↑(π / 2) - ↑x✝).sin = (↑x✝).cos
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (θ + ↑(π / 2)).cos = -θ.sin

Tactic:
induction θ using Real.Angle.induction_on

Goal state after:
case h
x✝ : ℝ
⊢ (↑x✝ + ↑(π / 2)).cos = -(↑x✝).sin
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (θ - ↑(π / 2)).cos = θ.sin

Tactic:
induction θ using Real.Angle.induction_on

Goal state after:
case h
x✝ : ℝ
⊢ (↑x✝ - ↑(π / 2)).cos = (↑x✝).sin
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ (↑(π / 2) - θ).cos = θ.sin

Tactic:
induction θ using Real.Angle.induction_on

Goal state after:
case h
x✝ : ℝ
⊢ (↑(π / 2) - ↑x✝).cos = (↑x✝).sin
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
abs_neg

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

Goal state before:
pp: case inr
ψ : Angle
⊢ |(-ψ.cos)| = |ψ.cos|

Tactic:
abs_neg

Goal state after:
case inr
ψ : Angle
⊢ |ψ.cos| = |ψ.cos|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : Angle
h : θ.toReal = ψ.toReal
⊢ θ = ψ

Tactic:
induction θ using Real.Angle.induction_on

Goal state after:
case h
ψ : Angle
x✝ : ℝ
h : (↑x✝).toReal = ψ.toReal
⊢ ↑x✝ = ψ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ ↑θ.toReal = θ

Tactic:
induction θ using Real.Angle.induction_on

Goal state after:
case h
x✝ : ℝ
⊢ ↑(↑x✝).toReal = ↑x✝
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ -π < θ.toReal

Tactic:
induction θ using Real.Angle.induction_on

Goal state after:
case h
x✝ : ℝ
⊢ -π < (↑x✝).toReal
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ θ.toReal ≤ π

Tactic:
induction θ using Real.Angle.induction_on

Goal state after:
case h
x✝ : ℝ
⊢ (↑x✝).toReal ≤ π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
⊢ toIocMod two_pi_pos (-π) θ.toReal = θ.toReal

Tactic:
induction θ using Real.Angle.induction_on

Goal state after:
case h
x✝ : ℝ
⊢ toIocMod two_pi_pos (-π) (↑x✝).toReal = (↑x✝).toReal
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = ↑(‖x‖ * ‖y‖) * (cos ↑(x.arg + y.arg) + sin ↑(x.arg + y.arg) * I)

Tactic:
cos_add_sin_I,

Goal state after:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = ↑(‖x‖ * ‖y‖) * cexp (↑(x.arg + y.arg) * I)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ cexp z ∈ slitPlane ↔ toIocMod Real.two_pi_pos (-π) z.im ≠ π

Tactic:
simp [mem_slitPlane_iff_arg, arg_exp]

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

Goal state before:
pp: θ : Angle
⊢ (θ + ↑π).tan = θ.tan

Tactic:
induction θ using Real.Angle.induction_on

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

Goal state before:
pp: θ ψ : Angle
h : 2 • θ + 2 • ψ = ↑π
⊢ ψ.tan = θ.tan⁻¹

Tactic:
induction θ using Real.Angle.induction_on

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

Goal state before:
pp: case inr
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : ↑(θ.toReal + ψ.toReal) = ↑π
⊢ |θ.toReal| + |ψ.toReal| = π

Tactic:
suffices |θ.toReal + ψ.toReal| = π by grind [toReal_neg_iff_sign_neg, abs_add_eq_add_abs_iff]

Goal state after:
case inr
θ ψ : Angle
h✝ : 2 • (θ + ψ) = 0
hs : θ.sign = ψ.sign
h0 : θ.sign ≠ 0
h : ↑(θ.toReal + ψ.toReal) = ↑π
⊢ |θ.toReal + ψ.toReal| = π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: hb₀ : -1 < 0
hb₁ : 0 < 1
⊢ Tendsto (fun x ↦ 0 ^ x) atTop (𝓝 0)

Tactic:
refine Tendsto.mono_right ?_ (Iff.mpr pure_le_nhds_iff rfl)

Goal state after:
hb₀ : -1 < 0
hb₁ : 0 < 1
⊢ Tendsto (fun x ↦ 0 ^ x) atTop (pure 0)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case e'_2
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
hψ' : (-ψ).sign = 1
hsa' : (-θ + -ψ).sign ≠ 1
⊢ |(θ + ψ).toReal| = |(-θ + -ψ).toReal|

Tactic:
simp [-neg_add_rev, ← neg_add, abs_toReal_neg]

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

Goal state before:
pp: case e'_3
θ ψ : Angle
hs : θ.sign = ψ.sign
hsa : θ.sign ≠ (θ + ψ).sign
h : θ.sign = -1
hθ' : (-θ).sign = 1
hψ' : (-ψ).sign = 1
hsa' : (-θ + -ψ).sign ≠ 1
⊢ 2 * π - (|θ.toReal| + |ψ.toReal|) = 2 * π - (|(-θ).toReal| + |(-ψ).toReal|)

Tactic:
simp [-neg_add_rev, ← neg_add, abs_toReal_neg]

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

Goal state before:
pp: x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ x ^ (y + ↑n) = x ^ y * x ^ n

Tactic:
ext; exact Real.rpow_add_natCast (mod_cast hx) _ _

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

Goal state before:
pp: case inr
p : ℝ × ℝ
hp : 0 < p.1
⊢ ContinuousAt (fun p ↦ p.1 ^ p.2) p

Tactic:
rw [continuousAt_congr (rpow_eq_nhds_of_pos hp)]
    refine continuous_exp.continuousAt.comp (ContinuousAt.mul ?_ continuous_snd.continuousAt)
    refine (continuousAt_log ?_).comp continuous_fst.continuousAt
    exact hp.ne'

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

Goal state before:
pp: x : ℝ≥0
n : ℕ
hn : n ≠ 0
⊢ (↑x ^ n) ^ (↑n)⁻¹ = ↑x

Tactic:
exact Real.pow_rpow_inv_natCast x.2 hn

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

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

Tactic:
by
  simp only [orderIsoRpow, one_div_one_div]
  rfl

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

Goal state before:
pp: case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : p ≠ 0
hx0 : x = 0
hp_pos : 0 < p
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
simp [hx0, hp_pos, hp_pos.ne.symm]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr.inr
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy✝ : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h₁ : r₁ • x = r₂ • y
r₃ r₄ : R
hr₃ : 0 < r₃
hr₄ : 0 < r₄
h₂ : r₃ • y = r₄ • z
⊢ (r₃ * r₁) • x = (r₂ * r₄) • z

Tactic:
mul_smul,

Goal state after:
case inr.inr.inr
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy✝ : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h₁ : r₁ • x = r₂ • y
r₃ r₄ : R
hr₃ : 0 < r₃
hr₄ : 0 < r₄
h₂ : r₃ • y = r₄ • z
⊢ r₃ • r₁ • x = (r₂ * r₄) • z
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr.inr
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy✝ : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h₁ : r₁ • x = r₂ • y
r₃ r₄ : R
hr₃ : 0 < r₃
hr₄ : 0 < r₄
h₂ : r₃ • y = r₄ • z
⊢ r₃ • r₁ • x = (r₂ * r₄) • z

Tactic:
mul_smul,

Goal state after:
case inr.inr.inr
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hxy : SameRay R x y
hyz : SameRay R y z
hy✝ : y = 0 → x = 0 ∨ z = 0
hx : x ≠ 0
hz : z ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h₁ : r₁ • x = r₂ • y
r₃ r₄ : R
hr₃ : 0 < r₃
hr₄ : 0 < r₄
h₂ : r₃ • y = r₄ • z
⊢ r₃ • r₁ • x = r₂ • r₄ • z
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr.inr
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
⊢ SameRay R (x + y) z

Tactic:
rcases hx.exists_pos hx₀ hz₀ with ⟨rx, rz₁, hrx, hrz₁, Hx⟩

Goal state after:
case inr.inr.inr
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y z : M
hx : SameRay R x z
hy : SameRay R y z
hx₀ : x ≠ 0
hy₀ : y ≠ 0
hz₀ : z ≠ 0
rx rz₁ : R
hrx : 0 < rx
hrz₁ : 0 < rz₁
Hx : rx • x = rz₁ • z
⊢ SameRay R (x + y) z
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
u : Rˣ
v : Ray R M
this : 0 < ↑u * ↑u
⊢ (u * u) • u⁻¹ • v = u • v

Tactic:
mul_smul,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
v : Ray R M
this : 0 < ↑u * ↑u
⊢ u • u • u⁻¹ • v = u • v
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_1.inl.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
hx0 : x = 0
⊢ ∃ g, ∑ i, g i • ![x, y] i = 0 ∧ ∃ i, g i ≠ 0

Tactic:
exact False.elim (hx hx0)

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_1.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
hx0 : x = 0
⊢ ∃ g, ∑ i, g i • ![x, y] i = 0 ∧ ∃ i, g i ≠ 0

Tactic:
exact False.elim (hx hx0)

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
h✝ : SameRay R x y
hx : x ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • y
⊢ (r₂⁻¹ * r₁) • x = y

Tactic:
mul_smul,

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 y : M
h✝ : SameRay R x y
hx : x ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • y
⊢ r₂⁻¹ • r₁ • x = y
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr.refine_2
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ v₁ = ((r₁ + r₂)⁻¹ * r₂) • (v₁ + v₂)

Tactic:
mul_smul,

Goal state after:
case inr.inr.refine_2
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ v₁ = (r₁ + r₂)⁻¹ • r₂ • (v₁ + v₂)
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case inr.inr.refine_3
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ v₂ = ((r₁ + r₂)⁻¹ * r₁) • (v₁ + v₂)

Tactic:
mul_smul,

Goal state after:
case inr.inr.refine_3
R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ v₂ : M
r₁ r₂ : R
h₁ : 0 < r₁
h₂ : 0 < r₂
H : r₁ • v₁ = r₂ • v₂
h₁₂ : 0 < r₁ + r₂
⊢ v₂ = (r₁ + r₂)⁻¹ • r₁ • (v₁ + v₂)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
a b : 𝕜
f : E →ᵃ[𝕜] F
h : a + b = 1
⊢ f (a • x + b • y) = a • f x + b • f y

Tactic:
simp only [Convex.combo_eq_smul_sub_add h, ← vsub_eq_sub]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
a b : 𝕜
f : E →ᵃ[𝕜] F
h : a + b = 1
⊢ f (b • (y -ᵥ x) + x) = b • (f y -ᵥ f x) + f 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
t : Set (AffineSubspace k P)
p : P
h : ∀ s ∈ t, p ∈ s
v : V
hv : v ∈ ⨅ s ∈ t, s.direction
s : AffineSubspace k P
hs : s ∈ t
⊢ v +ᵥ p ∈ s

Tactic:
vadd_mem_iff_mem_direction v (h s hs)

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
t : Set (AffineSubspace k P)
p : P
h : ∀ s ∈ t, p ∈ s
v : V
hv : v ∈ ⨅ s ∈ t, s.direction
s : AffineSubspace k P
hs : s ∈ t
⊢ v ∈ s.direction
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
S : Type u_7
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
V : S
hV : Absorbent 𝕜 ↑V
x : E
c : 𝕜
hc : c • x ∈ ↑V
hc' : c ∈ {0}ᶜ
⊢ c⁻¹ • c • x ∈ ↑V

Tactic:
exact SMulMemClass.smul_mem c⁻¹ hc

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

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst✝¹] U
h : 0 ∉ U
⊢ IsClosed[inst✝¹] (balancedCore 𝕜 U)

Tactic:
· have : balancedCore 𝕜 U = ∅ := by
      contrapose! h
      exact balancedCore_nonempty_iff.mp h
    rw [this]
    exact isClosed_empty

Goal state after: