mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c ↦ c • (y - x) + x
⊢ f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1

Tactic:
intro c hc

Goal state after:
case inr.inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c ↦ c • (y - x) + x
c : ℝ
hc : c ∈ f ⁻¹' closedBall x (dist y x)
⊢ c ∈ Icc (-1) 1
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
this : EqOn (fun x ↦ ‖x‖) id (Ioo a b)
⊢ (fun x ↦ ‖x‖) ⁻¹' Ioo (a * r) (b * r) = ball 0 (b * r) \ closedBall 0 (a * r)

Tactic:
ext x

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
this : EqOn (fun x ↦ ‖x‖) id (Ioo a b)
x : E
⊢ x ∈ (fun x ↦ ‖x‖) ⁻¹' Ioo (a * r) (b * r) ↔ x ∈ ball 0 (b * r) \ closedBall 0 (a * r)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: c : ℝ := cos (π / 5)
⊢ 4 * c ^ 2 + -(2 * c) + -1 = 0

Tactic:
← sub_eq_add_neg,

Goal state after:
c : ℝ := cos (π / 5)
⊢ 4 * c ^ 2 + -(2 * c) - 1 = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ Function.Periodic cosh (2 * ↑π * I)

Tactic:
convert! cosh_antiperiodic.periodic_two_mul using 1

Goal state after:
case e'_5
⊢ 2 * ↑π * I = 2 * (↑π * I)
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
γ : Path (p 0) (p (last n))
h₁ : ∀ (y : ↑I), γ y ∈ s
t : Fin (n + 1) → ↑I
ht : ∀ (i : Fin (n + 1)), γ (t i) = p i
⊢ ∃ γ t, (∀ (t : ↑I), γ t ∈ s) ∧ ∀ (i : Fin (n + 1)), γ (t i) = p i

Tactic:
exact ⟨γ, t, h₁, ht⟩

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : Unique X
f : C(X, Y)
⊢ const X ((fun f ↦ f default) f) = f

Tactic:
ext x

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : Unique X
f : C(X, Y)
x : X
⊢ (const X ((fun f ↦ f default) f)) x = f x
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : Y × X → Z
hg : Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ g (p.1, f p.2)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] g

Tactic:
have : Continuous fun p : X₀ × Y => g ((Prod.swap p).1, f (Prod.swap p).2) :=
    hg.comp continuous_swap
  have : Continuous fun p : X₀ × Y => (g ∘ Prod.swap) (f p.1, p.2) := this
  exact (hf.continuous_lift_prod_left this).comp continuous_swap

Goal state after:
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)
hfm : Monotone f
k n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x + f (2 * n) + -f (2 * n + 1) ≤ ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x

Tactic:
← sub_eq_add_neg,

Goal state after:
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)
hfm : Monotone f
k n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x + f (2 * n) - f (2 * n + 1) ≤ ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x
Module: Mathlib.Topology.Path

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

Tactic:
ext x

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t : ℝ
x : ↑I
⊢ (γ.truncate t t) x = ((refl (γ.extend t)).cast ⋯ ⋯) x
Module: Mathlib.Topology.Path

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

Tactic:
ext x

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
x : ↑I
⊢ (γ.truncate 0 1) x = (γ.cast ⋯ ⋯) x
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)
hfm : Monotone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i ≤
    ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i + -f (2 * n + 1) + f (2 * n + 1 + 1)

Tactic:
← sub_eq_add_neg,

Goal state after:
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)
hfm : Monotone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i ≤
    ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i - f (2 * n + 1) + f (2 * n + 1 + 1)
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 n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + f (2 * n) + -f (2 * n + 1)

Tactic:
← sub_eq_add_neg,

Goal state after:
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 n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + f (2 * n) - f (2 * n + 1)
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 n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x + -f (2 * n + 1) + f (2 * n + 2) ≤
    ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x

Tactic:
← sub_eq_add_neg,

Goal state after:
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 n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x - f (2 * n + 1) + f (2 * n + 2) ≤
    ∑ x ∈ Finset.range (2 * n + 1), (-1) ^ x * f x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: ⊢ (range fun x ↦ cexp (↑x * I)) = sphere 0 1

Tactic:
ext x

Goal state after:
x : ℂ
⊢ (x ∈ range fun x ↦ cexp (↑x * I)) ↔ x ∈ sphere 0 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

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

Tactic:
by
  rw [tan_eq_sin_div_cos, cos_arcsin]
  by_cases hx₁ : -1 ≤ x; swap
  · have h : √(1 - x ^ 2) = 0 := sqrt_eq_zero_of_nonpos (by nlinarith)
    rw [h]
    simp
  by_cases hx₂ : x ≤ 1; swap
  · have h : √(1 - x ^ 2) = 0 := sqrt_eq_zero_of_nonpos (by nlinarith)
    rw [h]
    simp
  rw [sin_arcsin hx₁ hx₂]

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

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

Tactic:
sub_neg_eq_add

Goal state after:
x : ℝ
⊢ π / 2 + arcsin x = π / 2 + arcsin x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.inr
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Tactic:
have hsin : 0 ≤ Real.sin θ := Real.sin_nonneg_of_mem_Icc ⟨by linarith, hθ⟩

Goal state after:
case neg.inr
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : π / 2 < θ
hθ : θ ≤ π
hcos : Real.cos θ < 0
hsin : 0 ≤ Real.sin θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x y : ℝ
hx : 0 < x
h : x < y
⊢ rexp (log x) < rexp (log y)

Tactic:
exp_log hx,

Goal state after:
x y : ℝ
hx : 0 < x
h : x < y
⊢ x < rexp (log y)
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x y : ℝ
hx : 0 < x
hy : 0 < y
⊢ rexp (log x) < rexp (log y) ↔ x < y

Tactic:
exp_log hx,

Goal state after:
x y : ℝ
hx : 0 < x
hy : 0 < y
⊢ x < rexp (log y) ↔ x < y
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ (↑(Real.log x)).re = (log ↑x).re

Tactic:
rw [log_re, ofReal_re, Complex.norm_of_nonneg hx]

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

Goal state before:
pp: ⊢ -↑π = ↑π

Tactic:
← coe_neg,

Goal state after:
⊢ ↑(-π) = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
nth_rw 1 [h]

Goal state after:
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ 2 • θ = ↑(2 • (π / 2)) ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mpr
θ ψ : ℝ
⊢ (∃ k, θ - ψ = 2 * π * ↑k) ∨ ↑θ = -↑ψ → cos θ = cos ψ

Tactic:
← coe_neg,

Goal state after:
case mpr
θ ψ : ℝ
⊢ (∃ k, θ - ψ = 2 * π * ↑k) ∨ ↑θ = ↑(-ψ) → cos θ = cos ψ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
mul_comm π _,

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

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

Tactic:
mul_comm π _,

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

Goal state before:
pp: case inl
n : ℤ
y : ℂ
⊢ 0 ^ (↑n * y) = (0 ^ y) ^ n

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Goal state after:
case inl.inl
y : ℂ
⊢ 0 ^ (↑0 * y) = (0 ^ y) ^ 0

case inl.inr
n : ℤ
y : ℂ
hn : n ≠ 0
⊢ 0 ^ (↑n * y) = (0 ^ y) ^ n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mpr.inl
θ ψ : ℝ
k : ℤ
H : θ - ψ = 2 * π * ↑k
⊢ 2 * sin (π * ↑k) * cos ((θ + ψ) / 2) = 0

Tactic:
mul_comm π _,

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

Goal state before:
pp: θ ψ : ℝ
k : ℤ
H : θ + ψ = 2 * (π * ↑k) + π
⊢ θ + ψ = 2 * ↑k * π + π

Tactic:
mul_comm π _,

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

Goal state before:
pp: θ : Angle
⊢ θ = ↑(π / 2) ∨ θ = -↑(π / 2) ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)

Tactic:
← coe_neg,

Goal state after:
θ : Angle
⊢ θ = ↑(π / 2) ∨ θ = ↑(-(π / 2)) ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inr
x : ℂ
hi : 0 < x.im
⊢ (-x).arg = x.arg - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0

Tactic:
· simp [hi, arg_neg_eq_arg_sub_pi_of_im_pos]

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

Goal state before:
pp: θ : Angle
⊢ (-↑θ.toReal).toReal = -θ.toReal ↔ θ ≠ ↑π

Tactic:
← coe_neg,

Goal state after:
θ : Angle
⊢ (↑(-θ.toReal)).toReal = -θ.toReal ↔ θ ≠ ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp
h : -π < -(↑π).toReal
h' : -(↑π).toReal ≤ π
⊢ False

Tactic:
simp at h

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

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

Tactic:
by
  rcases eq_or_ne θ π with rfl | h
  · simp
  · simp [toReal_neg_eq_neg_toReal_iff.2 h]

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

Goal state before:
pp: case neg
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : ¬θ = π
⊢ |(-↑θ).toReal| = θ

Tactic:
← coe_neg,

Goal state after:
case neg
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : ¬θ = π
⊢ |(↑(-θ)).toReal| = θ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : ℝ
k : ℤ
⊢ (↑θ).toReal = θ - 2 * ↑k * π ↔ θ ∈ Set.Ioc ((2 * ↑k - 1) * π) ((2 * ↑k + 1) * π)

Tactic:
rw [← sub_zero (θ : Angle), ← zsmul_zero k, ← coe_two_pi, ← coe_zsmul, ← coe_sub, zsmul_eq_mul, ←
    mul_assoc, mul_comm (k : ℝ), toReal_coe_eq_self_iff, Set.mem_Ioc]

Goal state after:
θ : ℝ
k : ℤ
⊢ -π < θ - 2 * ↑k * π ∧ θ - 2 * ↑k * π ≤ π ↔ (2 * ↑k - 1) * π < θ ∧ θ ≤ (2 * ↑k + 1) * π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h
x✝ : ℝ
⊢ Real.tan (x✝ + π) = Real.tan x✝

Tactic:
exact Real.tan_periodic _

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

Goal state before:
pp: case inr
θ : Angle
h : θ.sign = 0
⊢ -↑|θ.toReal| = θ

Tactic:
sign_eq_zero_iff

Goal state after:
case inr
θ : Angle
h : θ = 0 ∨ θ = ↑π
⊢ -↑|θ.toReal| = θ
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
⊢ |x ^ y| ≤ rexp (log x * y)

Tactic:
by
  refine (abs_rpow_le_abs_rpow x y).trans ?_
  by_cases hx : x = 0
  · by_cases hy : y = 0 <;> simp [hx, hy, zero_le_one]
  · rw [rpow_def_of_pos (abs_pos.2 hx), log_abs]

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

Goal state before:
pp: a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : 0 < x
⊢ rexp (a * (log x / (b * rexp (log x) + c))) = x ^ (a / (b * x + c))

Tactic:
exp_log hx,

Goal state after:
a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : 0 < x
⊢ rexp (a * (log x / (b * x + c))) = x ^ (a / (b * x + c))
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y z : ℝ
H : 0 = x
h : y + z = 0
⊢ 0 ^ y * 0 ^ z ≤ 1 * 1

Tactic:
by
          gcongr
          exacts [zero_rpow_nonneg z, zero_rpow_le_one y, zero_rpow_le_one z]

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:
by
  ext; exact Real.rpow_sub_intCast (mod_cast hx) _ _

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

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

Tactic:
by
  rw [← rpow_le_rpow_iff _ hy hz, rpow_inv_rpow] <;> positivity

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

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

Tactic:
mul_le_mul_right_of_neg (log_neg hx0 hx1)

Goal state after:
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
⊢ z ≤ y ↔ z ≤ y
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
f g : P1 →ᵃ[k] P2
h : f = g
⊢ f default = g default

Tactic:
by rw [h]

Goal state after:
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: case neg.refine_2.inr.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
m : Fin (Nat.succ 0).succ → R
hm : m 0 • x = -(m 1 • y)
hmne : ∃ i, m i ≠ 0
hm0 : 0 < m 0
hm1 : 0 < m 1
⊢ m 0 • x = m 1 • -y

Tactic:
rwa [smul_neg]

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

Goal state before:
pp: k : Type u_1
V1 : Type u_2
V2 : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V1
inst✝² : Module k V1
inst✝¹ : AddCommGroup V2
inst✝ : Module k V2
f : V1 →ᵃ[k] V2
⊢ ⇑f = ⇑f.linear + fun x ↦ f 0

Tactic:
ext x

Goal state after:
k : Type u_1
V1 : Type u_2
V2 : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V1
inst✝² : Module k V1
inst✝¹ : AddCommGroup V2
inst✝ : Module k V2
f : V1 →ᵃ[k] V2
x : V1
⊢ f x = (⇑f.linear + fun x ↦ f 0) x
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: k : Type u_10
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
f : k →ᵃ[k] k
a b : k
⊢ ⇑f = (fun x ↦ x + f 0) ∘ fun x ↦ x * (f 1 - f 0)

Tactic:
ext x

Goal state after:
k : Type u_10
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
f : k →ᵃ[k] k
a b x : k
⊢ f x = ((fun x ↦ x + f 0) ∘ fun x ↦ x * (f 1 - f 0)) x
Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Goal state before:
pp: k : Type u_10
V : Type u_11
P : Type u_12
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
⊢ ofLinearEquiv (LinearEquiv.refl k V) p p = refl k P

Tactic:
ext x

Goal state after:
k : Type u_10
V : Type u_11
P : Type u_12
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p x : P
⊢ (ofLinearEquiv (LinearEquiv.refl k V) p p) x = (refl k P) x
Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Goal state before:
pp: k : Type u_10
V : Type u_11
P : Type u_12
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
A B : V ≃ₗ[k] V
p₀ p₁ p₂ : P
⊢ (ofLinearEquiv A p₀ p₁).trans (ofLinearEquiv B p₁ p₂) = ofLinearEquiv (A ≪≫ₗ B) p₀ p₂

Tactic:
ext x

Goal state after:
k : Type u_10
V : Type u_11
P : Type u_12
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
A B : V ≃ₗ[k] V
p₀ p₁ p₂ x : P
⊢ ((ofLinearEquiv A p₀ p₁).trans (ofLinearEquiv B p₁ p₂)) x = (ofLinearEquiv (A ≪≫ₗ B) p₀ p₂) x
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₁ + r₂) • v₁

Tactic:
inv_smul_smul₀ h₁₂.ne'

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₁ = 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₁ + r₂) • v₂

Tactic:
inv_smul_smul₀ h₁₂.ne'

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₂ = v₂
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
hs : 0 ∈ s
⊢ ↑s -ᵥ ↑s = ↑s

Tactic:
ext x

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
hs : 0 ∈ s
x : V
⊢ x ∈ ↑s -ᵥ ↑s ↔ x ∈ ↑s
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
h : (↑s).Nonempty
⊢ directionOfNonempty h = s.direction

Tactic:
refine le_antisymm ?_ (Submodule.span_le.2 Set.Subset.rfl)
  rw [← SetLike.coe_subset_coe, directionOfNonempty, direction, Submodule.coe_set_mk,
    AddSubmonoid.coe_set_mk]
  exact vsub_set_subset_vectorSpan k _

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

Goal state before:
pp: case refine_1.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
h : x < y
a : 𝕜
ha : 0 ≤ a
hb : 0 ≤ 0
hab : a = 1
hz : x ∈ Ioc x y
⊢ ∃ a_1 b, 0 ≤ a_1 ∧ 0 < b ∧ a_1 + b = 1 ∧ a_1 * x + b * y = a * x + 0 * y

Tactic:
exact (hz.1.ne rfl).elim

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst✝⁸ : Semiring 𝕜
inst✝⁷ : PartialOrder 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : PosSMulMono 𝕜 β
f : E → β
h : IsLinearMap 𝕜 f
r : β
⊢ Convex 𝕜 {w | f w = r}

Tactic:
by
  simp_rw [le_antisymm_iff]
  exact (convex_halfSpace_le h r).inter (convex_halfSpace_ge h r)

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
⊢ ↑s.direction = s

Tactic:
ext x

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
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 : Submodule k V
⊢ (↑s).direction = s

Tactic:
ext x

Goal state after:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Submodule k V
x : V
⊢ x ∈ (↑s).direction ↔ x ∈ s
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
p : P
⊢ mk' p ⊤ = ⊤

Tactic:
ext x

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
p x : P
⊢ x ∈ mk' p ⊤ ↔ x ∈ ⊤
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: M : Type u_1
E : Type u_2
inst✝² : Bornology M
inst✝¹ : AddZeroClass E
inst✝ : DistribSMul M E
s₁ s₂ t : Set E
x : E
h₁ : Absorbent M s₁
h₂ : Absorbs M s₂ t
⊢ Absorbs M (s₁ + s₂) (x +ᵥ t)

Tactic:
← singleton_vadd

Goal state after:
M : Type u_1
E : Type u_2
inst✝² : Bornology M
inst✝¹ : AddZeroClass E
inst✝ : DistribSMul M E
s₁ s₂ t : Set E
x : E
h₁ : Absorbent M s₁
h₂ : Absorbs M s₂ t
⊢ Absorbs M (s₁ + s₂) ({x} +ᵥ t)
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
⊢ Absorbs 𝕜 s {x} ↔ ∀ᶠ (c : 𝕜) in 𝓝[≠] 0, c • x ∈ s

Tactic:
simp only [absorbs_iff_eventually_nhdsNE_zero, mapsTo_singleton]

Goal state after: