mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
inst✝ : IsFiniteMeasure μ
⊢ μ.InnerRegularWRT IsCompact MeasurableSet

Tactic:
convert! h.innerRegular with s

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
inst✝ : IsFiniteMeasure μ
s : Set α
⊢ MeasurableSet s ↔ MeasurableSet s ∧ μ s ≠ ∞
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: case isOpen
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : TopologicalSpace G
inst✝² : BorelSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s U : Set G
hU : IsOpen[inst✝³] U
⊢ U * closure[inst✝³] {1} = U

Tactic:
exact hU.mul_closure_one_eq

Goal state after:
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set α
f : α → ℝ≥0∞
⊢ (μ.withDensity f).restrict s = (μ.restrict s).withDensity f

Tactic:
by
  ext1 t ht
  rw [restrict_apply ht, withDensity_apply _ ht, withDensity_apply' _ (t ∩ s),
    restrict_restrict ht]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ ?m.55 t ≠ ∞

Tactic:
← measure_congr hst

Goal state after:
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
⊢ μ s ≠ ∞
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: x : ℝ
hx : ‖x‖ ≤ 1
⊢ 0 ≤ 1 - x ^ 2

Tactic:
by nlinarith [abs_le.mp hx]

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

Goal state before:
pp: z : ℂ
⊢ z ^ 2 ≤ 0 ↔ z.re = 0

Tactic:
nonpos_iff,

Goal state after:
z : ℂ
⊢ (z ^ 2).re ≤ 0 ∧ (z ^ 2).im = 0 ↔ z.re = 0
Module: Mathlib.Analysis.Complex.Order

Goal state before:
pp: z w : ℂ
⊢ ¬z ≤ w ↔ w.re < z.re ∨ z.im ≠ w.im

Tactic:
rw [le_def, not_and_or, not_le]

Goal state after:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: a b₁ b₂ : ℝ
⊢ (fun y ↦ ↑a + ↑y * I) '' [[b₁, b₂]] = {a} ×ℂ [[b₁, b₂]]

Tactic:
by
  rw [← preimage_equivRealProd_prod]
  ext x
  constructor
  · intro hx
    obtain ⟨x₁, hx₁, hx₁'⟩ := hx
    simp [← hx₁', mem_preimage, mem_prod, hx₁]
  · intro hx
    simp only [equivRealProd_apply, singleton_prod, mem_image, Prod.mk.injEq,
      exists_eq_right_right, mem_preimage] at hx
    obtain ⟨x₁, hx₁, hx₁', hx₁''⟩ := hx
    refine ⟨x.im, x₁, by simp⟩

Goal state after:
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: M : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
μ ν : Measure M
inst✝ : SFinite ν
s : ℝ≥0∞
⊢ map (fun x ↦ x.1 * x.2) (s • μ.prod ν) = s • map (fun x ↦ x.1 * x.2) (μ.prod ν)

Tactic:
Measure.map_smul

Goal state after:
M : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
μ ν : Measure M
inst✝ : SFinite ν
s : ℝ≥0∞
⊢ s • map (fun x ↦ x.1 * x.2) (μ.prod ν) = s • map (fun x ↦ x.1 * x.2) (μ.prod ν)
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ f g : NormedAddGroupHom V₁ V₂
⊢ ∃ C, ∀ (v : V₁), ‖(f.toAddMonoidHom + -g.toAddMonoidHom) v‖ ≤ C * ‖v‖

Tactic:
exact (f + -g).bound'

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

Goal state before:
pp: z : ℂ
R : Type u_1
inst✝¹ : NormedField R
inst✝ : NormedAlgebra R ℝ
r : R
x : ℂ
⊢ ‖(algebraMap R ℝ) r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
real_smul,

Goal state after:
z : ℂ
R : Type u_1
inst✝¹ : NormedField R
inst✝ : NormedAlgebra R ℝ
r : R
x : ℂ
⊢ ‖↑((algebraMap R ℝ) r) * x‖ ≤ ‖r‖ * ‖x‖
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
r : ℝ
⊢ im (z * ↑r) = im z * r

Tactic:
rw [mul_comm, im_ofReal_mul, mul_comm]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ re (r • z) = r * re z

Tactic:
real_smul_eq_coe_mul,

Goal state after:
K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ re (↑r * z) = r * re z
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ im (r • z) = r * im z

Tactic:
real_smul_eq_coe_mul,

Goal state after:
K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ im (↑r * z) = r * im z
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
L : SummationFilter α
f : α → 𝕜
c : 𝕜
⊢ HasSum (fun x ↦ re (f x)) (re c) L ∧ HasSum (fun x ↦ im (f x)) (im c) L → HasSum f c L

Tactic:
rintro ⟨h₁, h₂⟩

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
L : SummationFilter α
f : α → 𝕜
c : 𝕜
h₁ : HasSum (fun x ↦ re (f x)) (re c) L
h₂ : HasSum (fun x ↦ im (f x)) (im c) L
⊢ HasSum f c L
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z w : K
⊢ im (z / w) = im z * re w / normSq w - re z * im w / normSq w

Tactic:
simp only [div_eq_mul_inv, mul_assoc, sub_eq_add_neg, add_comm, neg_mul, mul_neg,
    rclike_simps]

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝³ : RCLike K
inst✝² : NormedField E
inst✝¹ : CharZero E
inst✝ : NormedSpace K E
ι : Type u_3
s : Finset ι
f : ι → E
x✝¹ : ℕ
x✝ : E
⊢ ‖(↑x✝¹)⁻¹ • x✝‖ = (↑x✝¹)⁻¹ • ‖x✝‖

Tactic:
rw [norm_nnqsmul K]

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
⊢ Tendsto (↑e.symm) (𝓝 (↑e x)) (𝓝 x)

Tactic:
by
  simpa only [ContinuousAt, e.left_inv hx] using e.continuousAt_symm (e.map_source hx)

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
hz : 0 < z
⊢ 0 < z⁻¹

Tactic:
rw [pos_iff_exists_ofReal] at hz

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
hz : ∃ x > 0, ↑x = z
⊢ 0 < z⁻¹
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
h : (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ ↑x * y) a b) ((fun x y ↦ ↑x * y) a c)
a' : ℝ
ha1 : a' > 0
ha2 : ↑a' = ↑a
⊢ b ≤ c

Tactic:
rw [← sub_nonneg]

Goal state after:
K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
h : (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ ↑x * y) a b) ((fun x y ↦ ↑x * y) a c)
a' : ℝ
ha1 : a' > 0
ha2 : ↑a' = ↑a
⊢ 0 ≤ c - b
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : K
⊢ ‖re (x - y)‖ₑ ≤ ‖x - y‖ₑ

Tactic:
rw [enorm_le_iff_norm_le]

Goal state after:
K : Type u_1
inst✝ : RCLike K
x y : K
⊢ ‖re (x - y)‖ ≤ ‖x - y‖
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : K
⊢ ‖im (x - y)‖ₑ ≤ ‖x - y‖ₑ

Tactic:
rw [enorm_le_iff_norm_le]

Goal state after:
K : Type u_1
inst✝ : RCLike K
x y : K
⊢ ‖im (x - y)‖ ≤ ‖x - y‖
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : K
⊢ ‖im (x - y)‖ₑ ≤ ‖x - y‖ₑ

Tactic:
by rw [enorm_le_iff_norm_le]; exact norm_im_le_norm (x - y)

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

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (∃ c, IsBigOWith c l (fun x ↦ ‖f' x‖) g) ↔ ∃ c, IsBigOWith c l f' g

Tactic:
exact exists_congr fun _ => isBigOWith_norm_left

Goal state after:
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''
f'' : α → E''
l : Filter α
c : F''
⊢ (f'' =O[l] fun _x ↦ c) ↔ (c = 0 → f'' =ᶠ[l] 0) ∧ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f'' x‖

Tactic:
refine ⟨fun h => ⟨fun hc => isBigO_zero_right_iff.1 (by rwa [← hc]), h.isBoundedUnder_le⟩, ?_⟩

Goal state after:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
l : Filter α
c : F''
⊢ ((c = 0 → f'' =ᶠ[l] 0) ∧ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f'' x‖) → f'' =O[l] fun _x ↦ c
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cosh x ^ 2 - sinh x ^ 2 = 1

Tactic:
by
  rw [sq_sub_sq, cosh_add_sinh, cosh_sub_sinh, ← exp_add, add_neg_cancel, exp_zero]

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

Goal state before:
pp: case hba
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
x : ℕ
a✝ : x ∈ range (j - n)
⊢ ↑n.factorial * ↑n.succ ^ x ≤ ↑(x + n).factorial

Tactic:
rw [← Nat.cast_pow, ← Nat.cast_mul, Nat.cast_le, add_comm]

Goal state after:
case hba
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
x : ℕ
a✝ : x ∈ range (j - n)
⊢ n.factorial * n.succ ^ x ≤ (n + x).factorial
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
⊢ rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n + 1) / (↑n.factorial * ↑n)

Tactic:
have h3 : |x| = x := by simpa
  have h4 : |x| ≤ 1 := by rwa [h3]
  have h' := Real.exp_bound h4 hn
  rw [h3] at h'
  have h'' := (abs_sub_le_iff.1 h').1
  have t := sub_le_iff_le_add'.1 h''
  simpa [mul_div_assoc] using t

Goal state after:
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
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
a : ℝ
ha : a ∈ Set.Ioo 0 R
H : f =O[atTop] fun x ↦ a ^ x
C : ℝ
hC₀ : C > 0
hC : ∀ ⦃x : ℕ⦄, a ^ x ≠ 0 → ‖f x‖ ≤ C * ‖a ^ x‖
n : ℕ
⊢ |f n| ≤ C * a ^ n

Tactic:
simpa only [Real.norm_eq_abs, abs_pow, abs_of_nonneg ha.1.le] using hC (pow_ne_zero n ha.1.ne')

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

Goal state before:
pp: α : Type u_1
x y z : ℝ
l : Filter α
⊢ Tendsto (fun x ↦ ⟨rexp x, ⋯⟩) atTop atTop

Tactic:
rw [tendsto_Ioi_atTop]; simp only [tendsto_exp_atTop]

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:
simp [div_eq_mul_inv, hs.mul_closedBall_one hδ]

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

Goal state before:
pp: α : Type u_1
R✝ : Type u_2
S : Type u_3
inst✝⁷ : Field R✝
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
v w : AbsoluteValue R✝ S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
_i : OrderTopology S
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
⊢ HasSummableGeomSeries R

Tactic:
constructor
  intro x hx
  have h1 : Summable fun n : ℕ ↦ ‖x‖ ^ n := summable_geometric_of_lt_one (norm_nonneg _) hx
  exact h1.of_norm_bounded_eventually_nat (eventually_norm_pow_le x)

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

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
⊢ x +ᵥ closedBall 0 r = closedBall x r

Tactic:
vadd_closedBall_zero

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
⊢ closedBall x r = closedBall x r
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ ∀ ⦃y : X⦄, y ∈ {x} → JoinedIn {x} x y

Tactic:
rintro y rfl

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
y : X
⊢ JoinedIn {y} y y
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ IsPathConnected {x}

Tactic:
by
  refine ⟨x, rfl, ?_⟩
  rintro y rfl
  exact JoinedIn.refl rfl

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

Goal state before:
pp: case refine_1
x r : ℝ
hr : r ≤ ‖↑x‖
⊢ r ≤ |x - ↑(round x)|

pp: case refine_2
x : ℝ
⊢ ∀ (m : ℝ), ↑m = ↑x → |x - ↑(round x)| ≤ |m|

Tactic:
· rw [abs_sub_round_eq_min, le_inf_iff]
    rw [le_norm_iff] at hr
    constructor
    · simpa [abs_of_nonneg] using hr (fract x)
    · simpa [abs_sub_comm (fract x)] using hr (fract x - 1) (by simp)

Goal state after:
case refine_2
x : ℝ
⊢ ∀ (m : ℝ), ↑m = ↑x → |x - ↑(round x)| ≤ |m|
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p : ℝ
hp : p ≠ 0
x✝ : AddCircle p
ε : ℝ
hε : |p| / 2 ≤ ε
x : AddCircle p
⊢ x ∈ closedBall x✝ ε

Tactic:
by
    simpa only [mem_closedBall, dist_eq_norm] using (norm_le_half_period p hp).trans hε

Goal state after:
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
a b : X
γ : Path a b
t : ℝ
⊢ γ.extend (min t t) = γ.extend t

Tactic:
by rw [min_self]

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

Goal state before:
pp: case inl
hx : 0 ≤ 0
⊢ 0 < log 0 ↔ 1 < 0

Tactic:
simp [zero_le_one]

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

Goal state before:
pp: case inl
hx : 0 ≤ 0
⊢ log 0 ≤ 0 ↔ 0 ≤ 1

Tactic:
simp [zero_le_one]

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

Goal state before:
pp: ⊢ π / 2 ≠ 0

Tactic:
exact div_ne_zero Real.pi_ne_zero two_ne_zero

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

Goal state before:
pp: x : ℂ
hx_re : x.re < 0
hx_im : 0 < x.im
⊢ arg =ᶠ[𝓝 x] fun x ↦ Real.arcsin ((-x).im / ‖x‖) + π

Tactic:
suffices h_forall_nhds : ∀ᶠ y : ℂ in 𝓝 x, y.re < 0 ∧ 0 < y.im from
    h_forall_nhds.mono fun y hy => arg_of_re_neg_of_im_nonneg hy.1 hy.2.le
  refine IsOpen.eventually_mem ?_ (⟨hx_re, hx_im⟩ : x.re < 0 ∧ 0 < x.im)
  exact
    IsOpen.and (isOpen_lt continuous_re continuous_zero) (isOpen_lt continuous_zero continuous_im)

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

Goal state before:
pp: θ ψ : Angle
⊢ θ = ψ ↔ θ.sign = ψ.sign ∧ |θ.toReal| = |ψ.toReal|

Tactic:
grind [toReal_neg_iff_sign_neg]

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

Goal state before:
pp: x : ℝ
⊢ x ^ 0 = 1

Tactic:
by simp [rpow_def]

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

Goal state before:
pp: x : ℝ
⊢ x ^ 1 = x

Tactic:
by simp [rpow_def]

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

Goal state before:
pp: x : ℝ
⊢ 1 ^ x = 1

Tactic:
by simp [rpow_def]

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

Goal state before:
pp: case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ 0 < ‖x‖

Tactic:
norm_pos_iff

Goal state after:
case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ x ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case h₁
x : ℝ
hx : 0 ≤ x
y : ℝ
z : ℂ
⊢ -π < (log ↑x * ↑y).im

Tactic:
rw [← ofReal_log hx, ← ofReal_mul, ofReal_im, neg_lt_zero]; exact Real.pi_pos

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

Goal state before:
pp: case neg.hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ 0 ≤ x

pp: case hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ 0 ≤ x * y

Tactic:
all_goals positivity

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

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 ≤ x

pp: case hx
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 ≤ y

pp: case hx
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 ≤ x

pp: case ha
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 < x ^ z

pp: case hb
x y z : ℝ
hx : 0 < x
hxy : x < y
hz : z < 0
this : 0 < y
⊢ 0 < y ^ z

Tactic:
all_goals positivity

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

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ x

pp: case hx
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ y

pp: case hx
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 ≤ x

pp: case ha
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 < x ^ z

pp: case hb
x y z : ℝ
hx : 0 < x
hxy : x ≤ y
hz : z ≤ 0
this : 0 < y
⊢ 0 < y ^ z

Tactic:
all_goals positivity

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

Goal state before:
pp: x : ℝ≥0
y : ℝ
h : 0 ≤ y
⊢ ↑(x ^ y) = ↑x ^ y

Tactic:
by_cases hx : x = 0
  · rcases le_iff_eq_or_lt.1 h with (H | H)
    · simp [hx, H.symm]
    · simp [hx, zero_rpow_of_pos H, NNReal.zero_rpow (ne_of_gt H)]
  · exact coe_rpow_of_ne_zero hx _

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

Goal state before:
pp: x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
⊢ ContinuousAt (fun p ↦ ↑p.1 ^ p.2) (x, y)

Tactic:
rcases lt_trichotomy (0 : ℝ) x with (hx | rfl | hx)

Goal state after:
case inl
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : 0 < x
⊢ ContinuousAt (fun p ↦ ↑p.1 ^ p.2) (x, y)

case inr.inl
y : ℂ
h : 0 < y.re ∨ 0 ≠ 0
⊢ ContinuousAt (fun p ↦ ↑p.1 ^ p.2) (0, y)

case inr.inr
x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
⊢ ContinuousAt (fun p ↦ ↑p.1 ^ p.2) (x, y)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
hy : 0 < y
⊢ x ^ y < 1 ↔ x < 1

Tactic:
rw [← Real.rpow_lt_rpow_iff hx zero_le_one hy, Real.one_rpow]

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

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

Tactic:
simp [*, hz.not_gt]

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

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

Tactic:
simp [*, hz.not_gt]

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

Goal state before:
pp: 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

Tactic:
simp [*, hz.not_gt]

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

Goal state before:
pp: 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

Tactic:
simp [*, hz.not_gt]

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

Goal state before:
pp: x : ℝ≥0∞
z : ℝ
hx1 : 0 < x
hx2 : x ≤ 1
hz : z < 0
⊢ 1 ≤ x ^ z

Tactic:
lift x to ℝ≥0 using ne_of_lt (lt_of_le_of_lt hx2 coe_lt_top)
  simp only [coe_le_one_iff, coe_pos] at hx1 hx2 ⊢
  simp [← coe_rpow_of_ne_zero (ne_of_gt hx1),
    NNReal.one_le_rpow_of_pos_of_le_one_of_nonpos hx1 hx2 (le_of_lt hz)]

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
⊢ midpoint R (x + -y) (x + y) = x

Tactic:
← vadd_eq_add,

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

Tactic:
← vadd_eq_add,

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
⊢ midpoint R (x +ᵥ -y) (x +ᵥ y) = x
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
a x b c : E
⊢ a + x ∈ [a + b -[𝕜] a + c] ↔ x ∈ [b -[𝕜] c]

Tactic:
← vadd_eq_add,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a x b c : E
⊢ a +ᵥ x ∈ [a +ᵥ b -[𝕜] a +ᵥ c] ↔ x ∈ [b -[𝕜] c]
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
a x b c : E
⊢ a + x ∈ openSegment 𝕜 (a + b) (a + c) ↔ x ∈ openSegment 𝕜 b c

Tactic:
← vadd_eq_add,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a x b c : E
⊢ a +ᵥ x ∈ openSegment 𝕜 (a +ᵥ b) (a +ᵥ c) ↔ x ∈ openSegment 𝕜 b c
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Ring 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Invertible 2
x y : E
⊢ x = midpoint 𝕜 (x - y) (x + y)

Tactic:
rw [midpoint_sub_add]

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

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y : 𝕜
hxy : x ≠ y
h : y < x
⊢ openSegment 𝕜 x y = Ioo (min x y) (max x y)

Tactic:
· rw [openSegment_symm, openSegment_eq_Ioo h, max_eq_left h.le, min_eq_right h.le]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: case p
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
v : V
x✝ : P
| x✝ ∈ ↑s ∧ x✝ -ᵥ p = -v

Tactic:
rw [← neg_vsub_eq_vsub_rev, neg_inj]

Goal state after:
case p
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
v : V
x✝ : P
| x✝ ∈ ↑s ∧ p -ᵥ x✝ = v
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

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

Tactic:
have hpv : ((v +ᵥ p) -ᵥ p : V) ∈ (⊤ : AffineSubspace k P).direction :=
    vsub_mem_direction (mem_top k V _) (mem_top k 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
S : AffineSpace V P
p : P
v : V
_hv : v ∈ ⊤
hpv : (v +ᵥ p) -ᵥ p ∈ ⊤.direction
⊢ v ∈ ⊤.direction