mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
v : V₁
⊢ f (φ v) = g (φ v)

Tactic:
← comp_apply,

Goal state after:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
v : V₁
⊢ (f.comp φ) v = g (φ v)
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝² : SMul R ℝ
inst✝¹ : SMul S ℝ
inst✝ : SMulCommClass R S ℝ
r : R
s : S
x : ℂ
⊢ (r • s • x).re = (s • r • x).re

Tactic:
simp [smul_re, smul_im, smul_comm]

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

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝² : SMul R ℝ
inst✝¹ : SMul S ℝ
inst✝ : SMulCommClass R S ℝ
r : R
s : S
x : ℂ
⊢ (r • s • x).im = (s • r • x).im

Tactic:
simp [smul_re, smul_im, smul_comm]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
⊢ Semiring.toNatAlgebra = instAlgebraOfReal

Tactic:
by
  with_reducible_and_instances rfl

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

Goal state before:
pp: R : Type u_1
S : Type u_2
⊢ Ring.toIntAlgebra ℂ = instAlgebraOfReal

Tactic:
by
  with_reducible_and_instances rfl

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

Goal state before:
pp: R : Type u_1
S : Type u_2
⊢ Module.restrictScalars ℝ ℂ ℂ = instModule

Tactic:
by
  with_reducible_and_instances rfl

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

Goal state before:
pp: A : Type u_1
inst✝ : Ring A
inst : Algebra ℂ A
⊢ Algebra.toModule = Module.complexToReal A

Tactic:
by
  with_reducible_and_instances rfl

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ z - (starRingEnd K) z = ↑(re z) + ↑(im z) * I - (↑(re z) - ↑(im z) * I)

Tactic:
rw [re_add_im, ← conj_eq_re_sub_im]

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

Goal state before:
pp: A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
⊢ ℑ ∘ₗ (selfAdjoint.submodule ℝ A).subtype = 0

Tactic:
by
  ext; simp [imaginaryPart]

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

Goal state before:
pp: case inr
K : Type u_1
inst✝ : RCLike K
z : K
h₀ : z ≠ 0
⊢ z⁻¹ = (starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹

Tactic:
apply inv_eq_of_mul_eq_one_right
    rw [← mul_assoc, mul_conj, ofReal_inv, ofReal_pow, mul_inv_cancel₀]
    simpa

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

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
x : A
⊢ ↑(ℜ x) * ↑(ℑ x) - ↑(ℑ x) * ↑(ℜ x) = 0 ↔ Commute ↑(ℜ x) ↑(ℑ x)

Tactic:
sub_eq_zero,

Goal state after:
A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
x : A
⊢ ↑(ℜ x) * ↑(ℑ x) = ↑(ℑ x) * ↑(ℜ x) ↔ Commute ↑(ℜ x) ↑(ℑ x)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : K
⊢ edist (re x) (re y) ≤ ↑1 * edist x y

Tactic:
simp only [ENNReal.coe_one, one_mul, edist_eq_enorm_sub]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : K
⊢ edist (im x) (im y) ≤ ↑1 * edist x y

Tactic:
simp only [ENNReal.coe_one, one_mul, edist_eq_enorm_sub]

Goal state after:
K : Type u_1
inst✝ : RCLike K
x y : K
⊢ ‖im x - im y‖ₑ ≤ ‖x - y‖ₑ
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case mpr
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
⊢ (∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖f x‖ ≤ ‖g x‖) → f =o[l] g

Tactic:
refine fun H => isLittleO_iff.2 fun ε ε0 => ?_

Goal state after:
case mpr
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : ∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖f x‖ ≤ ‖g x‖
ε : ℝ
ε0 : 0 < ε
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ ε * ‖g x‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c c' : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : IsBigOWith c l f g
hgk : IsBigOWith c' l g k
hc : 0 ≤ c
⊢ IsBigOWith (c * c') l f k

Tactic:
by
  simp only [IsBigOWith_def] at *
  filter_upwards [hfg, hgk] with x hx hx'
  calc
    ‖f x‖ ≤ c * ‖g x‖ := hx
    _ ≤ c * (c' * ‖k x‖) := by gcongr
    _ = c * c' * ‖k x‖ := (mul_assoc _ _ _).symm

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
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
h : ∀ i ∈ s, ∃ c, IsBigOWith c l (A i) g
⊢ ∃ c, IsBigOWith c l (∑ i ∈ s, A i) g

Tactic:
choose! C hC using h

Goal state after:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
C : ι → ℝ
hC : ∀ i ∈ s, IsBigOWith (C i) l (A i) g
⊢ ∃ c, IsBigOWith c l (∑ i ∈ s, A i) g
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (f =O[l] fun x ↦ ‖f' x‖) ↔ f =O[l] f'

Tactic:
isBigO_norm_right

Goal state after:
α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ f =O[l] f' ↔ f =O[l] f'
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x y : ℂ
j m : ℕ
x✝ : m ∈ range j
⊢ (∑ m_1 ∈ range (m + 1), x ^ m_1 * y ^ (m - m_1) * ↑(m.choose m_1)) * (↑m.factorial)⁻¹ =
    ∑ k ∈ range (m + 1), x ^ k / ↑k.factorial * (y ^ (m - k) / ↑(m - k).factorial)

Tactic:
sum_mul

Goal state after:
x y : ℂ
j m : ℕ
x✝ : m ∈ range j
⊢ ∑ i ∈ range (m + 1), x ^ i * y ^ (m - i) * ↑(m.choose i) * (↑m.factorial)⁻¹ =
    ∑ k ∈ range (m + 1), x ^ k / ↑k.factorial * (y ^ (m - k) / ↑(m - k).factorial)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: ⊢ sin 0 = 0

Tactic:
by simp [sin]

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

Goal state before:
pp: case calc_2
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ∑ i ∈ range k, ‖x‖ ^ (n + i) / (↑n.factorial * ↑n.succ ^ i) =
    ∑ i ∈ range k, ‖x‖ ^ n / ↑n.factorial * (‖x‖ ^ i / ↑n.succ ^ i)

Tactic:
simp only [pow_add, div_eq_inv_mul, mul_inv, mul_left_comm, mul_assoc]

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

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

Tactic:
by simp [sin]

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

Goal state before:
pp: x y : ℝ
⊢ 2 * sin x * sin y = cos (x - y) - cos (x + y)

Tactic:
simp [cos_add, cos_sub]
  ring

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

Goal state before:
pp: x y : ℝ
⊢ 2 * cos x * cos y = cos (x - y) + cos (x + y)

Tactic:
simp [cos_add, cos_sub]
  ring

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

Goal state before:
pp: x : ℝ
⊢ sin x ^ 2 ≤ 1

Tactic:
rw [← sin_sq_add_cos_sq x]; exact le_add_of_nonneg_right (sq_nonneg _)

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

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm✝ : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
n : ℕ
hnm : n ≥ m
⊢ a + a < k • ε + (k • ε + 1 • ε)

Tactic:
one_nsmul

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm✝ : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
n : ℕ
hnm : n ≥ m
⊢ a + a < k • ε + (k • ε + ε)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
⊢ Disjoint (closedBall x δ) (ball y ε) ↔ δ + ε ≤ dist x y

Tactic:
by
  rw [disjoint_comm, disjoint_ball_closedBall_iff hε hδ, add_comm, dist_comm]

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
⊢ (n + k).descFactorial k = n ^ k + ∑ i ∈ Finset.range k, (fun i ↦ P.coeff i) i * n ^ i

Tactic:
conv_lhs => rw [A, mP.as_sum, 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) =
    n ^ k + ∑ i ∈ Finset.range k, (fun i ↦ P.coeff i) i * n ^ i
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case refine_1
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : s ∈ 𝓝 (const X c)
⊢ ∃ i, (IsCompact i.1 ∧ p i.2) ∧ {f | MapsTo (⇑f) i.1 (U i.2)} ⊆ s

Tactic:
rcases ContinuousMap.mem_nhds_iff.mp hs with ⟨S, hSf, hS, hSsub⟩

Goal state after:
case refine_1
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : s ∈ 𝓝 (const X c)
S : Set (Set X × Set Y)
hSf : S.Finite
hS : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K ∧ IsOpen[inst✝] U ∧ MapsTo (⇑(const X c)) K U
hSsub : {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g) K U} ⊆ s
⊢ ∃ i, (IsCompact i.1 ∧ p i.2) ∧ {f | MapsTo (⇑f) i.1 (U i.2)} ⊆ s
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
v : ℕ → α := fun n ↦ if n < N then 0 else u n
hC : 0 ≤ C
this : ∀ n ≥ N, u n = v n
⊢ CauchySeq fun n ↦ ∑ k ∈ Finset.range (n + 1), u k

Tactic:
apply cauchySeq_sum_of_eventually_eq this
    (NormedAddCommGroup.cauchy_series_of_le_geometric' hr₁ _)

Goal state after:
α : Type u_1
inst✝ : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
v : ℕ → α := ⋯
hC : 0 ≤ C
this : ∀ n ≥ N, u n = v n
⊢ ℝ

α : Type u_1
inst✝ : SeminormedAddCommGroup α
C : ℝ
u : ℕ → α
N : ℕ
r : ℝ
hr₀ : 0 < r
hr₁ : r < 1
h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n
v : ℕ → α := ⋯
hC : 0 ≤ C
this : ∀ n ≥ N, u n = v n
⊢ ∀ (n : ℕ), ‖v n‖ ≤ ?m.115 * r ^ n
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
⊢ IsPathConnected F → ∃ x ∈ F, pathComponentIn F x = F

Tactic:
rintro ⟨x, x_in, h⟩

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
⊢ ∃ x ∈ F, pathComponentIn F x = F
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
⊢ (∃ x ∈ F, pathComponentIn F x = F) → IsPathConnected F

Tactic:
rintro ⟨x, x_in, h⟩

Goal state after:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn F x = F
⊢ IsPathConnected F
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: ι : Type u_3
Z : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (Z i)
s : (i : ι) → Set (Z i)
h : ∀ (i : ι), IsPathConnected (s i)
⊢ IsPathConnected (univ.pi s)

Tactic:
choose x hx hjoin using h

Goal state after:
ι : Type u_3
Z : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (Z i)
s : (i : ι) → Set (Z i)
x : (i : ι) → Z i
hx : ∀ (i : ι), x i ∈ s i
hjoin : ∀ (i : ι) ⦃y : Z i⦄, y ∈ s i → JoinedIn (s i) (x i) y
⊢ IsPathConnected (univ.pi s)
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
γ : Path x y
γ' : Path y z
f : X → Y
h : Continuous[inst✝¹, inst✝] f
⊢ (γ.trans γ').map h = (γ.map h).trans (γ'.map h)

Tactic:
by
  ext t
  rw [trans_apply, map_coe, Function.comp_apply, trans_apply, map_coe, map_coe]
  grind

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

Goal state before:
pp: p x ε : ℝ
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε = ⋃ z, closedBall (x + z • p) ε

Tactic:
rcases eq_or_ne p 0 with (rfl | hp)
  · simp [iUnion_const]
  ext y
  simp only [dist_eq_norm, mem_preimage, mem_closedBall, zsmul_eq_mul, mem_iUnion, Real.norm_eq_abs,
    ← QuotientAddGroup.mk_sub, norm_eq, ← sub_sub]
  refine ⟨fun h => ⟨round (p⁻¹ * (y - x)), h⟩, ?_⟩
  rintro ⟨n, hn⟩
  rw [← mul_le_mul_iff_right₀ (abs_pos.mpr <| inv_ne_zero hp), ← abs_mul, mul_sub, mul_comm _ p,
    inv_mul_cancel_left₀ hp] at hn ⊢
  exact (round_le (p⁻¹ * (y - x)) n).trans hn

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
⊢ γ.extend (min 0 0) = a

Tactic:
min_self,

Goal state after:
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
⊢ γ.extend 0 = a
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
⊢ γ.extend (min 1 1) = b

Tactic:
min_self,

Goal state after:
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
⊢ γ.extend 1 = b
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case mp
x : ℝ
⊢ π / 2 - arcsin x ≤ π / 4 → π / 4 ≤ arcsin x

Tactic:
intro
      linarith

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

Goal state before:
pp: case mpr
x : ℝ
⊢ π / 4 ≤ arcsin x → π / 2 - arcsin x ≤ π / 4

Tactic:
intro
      linarith

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

Goal state before:
pp: ψ θ : Angle
⊢ 2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑π

Tactic:
two_zsmul_eq_iff

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

Goal state before:
pp: x : ℂ
hx : x.arg ≠ π
⊢ (if x.arg = π then -(starRingEnd ℂ) (log x) else -log x) = -log x

Tactic:
if_neg hx

Goal state after:
x : ℂ
hx : x.arg ≠ π
⊢ -log x = -log x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case refine_2
s : Set ℂ
hs : s.Countable
⊢ (cexp ⁻¹' s).Countable

Tactic:
rw [← Set.biUnion_preimage_singleton]
    refine hs.biUnion fun z hz => ?_
    by_cases! h : ∃ w, exp w = z
    · rcases h with ⟨w, rfl⟩
      simp only [Set.preimage, Set.mem_singleton_iff, exp_eq_exp_iff_exists_int, Set.ofPred_exists]
      exact Set.countable_iUnion fun m => Set.countable_singleton _
    · simp [Set.preimage, h]

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

Goal state before:
pp: case mp
x a : ℂ
⊢ 0 ^ x = a → x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
intro hyp

Goal state after:
case mp
x a : ℂ
hyp : 0 ^ x = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
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
θ : Angle
x✝ : ℝ
⊢ θ.cos = (↑x✝).cos ↔ θ = ↑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
θ : Angle
x✝ : ℝ
⊢ θ.sin = (↑x✝).sin ↔ θ = ↑x✝ ∨ θ + ↑x✝ = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x n : ℂ
hx : x.arg ≠ π
⊢ (if x.arg = π then (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)⁻¹ else (x ^ n)⁻¹) = (x ^ n)⁻¹

Tactic:
if_neg hx

Goal state after:
x n : ℂ
hx : x.arg ≠ π
⊢ (x ^ n)⁻¹ = (x ^ n)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : ℝ
⊢ ∃ k, toIocMod two_pi_pos ψ θ - θ = 2 * π * ↑k

Tactic:
refine ⟨-toIocDiv two_pi_pos ψ θ, ?_⟩

Goal state after:
θ ψ : ℝ
⊢ toIocMod two_pi_pos ψ θ - θ = 2 * π * ↑(-toIocDiv two_pi_pos ψ θ)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h
ψ : Angle
x✝ : ℝ
h : (↑x✝).toReal = ψ.toReal
⊢ ↑x✝ = ψ

Tactic:
induction ψ using Real.Angle.induction_on

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

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

Tactic:
rw [← toReal_inj, toReal_neg_pi_div_two]

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

Goal state before:
pp: x n : ℂ
hx : x.arg ≠ π
⊢ (if x.arg = π then x ^ n else (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)) = (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)

Tactic:
if_neg hx

Goal state after:
x n : ℂ
hx : x.arg ≠ π
⊢ (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n) = (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h
ψ : Angle
x✝ : ℝ
h : 2 • ↑x✝ + 2 • ψ = ↑π
⊢ ψ.tan = (↑x✝).tan⁻¹

Tactic:
induction ψ using Real.Angle.induction_on

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

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

Tactic:
rw [abs_eq_self.2 (toReal_nonneg_iff_sign_nonneg.2 h), coe_toReal]

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

Goal state before:
pp: case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt ((Real.Angle.coe ∘ arg) ∘ id) x

Tactic:
(funext_iff.2 fun _ => (neg_neg _).symm : (id : ℂ → ℂ) = Neg.neg ∘ Neg.neg),

Goal state after:
case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
⊢ ContinuousAt ((Real.Angle.coe ∘ arg) ∘ Neg.neg ∘ Neg.neg) x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ x ^ y = if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)

Tactic:
by
  simp only [rpow_def, Complex.cpow_def]; split_ifs <;>
  simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul,
      (Complex.ofReal_mul _ _).symm, Complex.exp_ofReal_re, Complex.ofReal_eq_zero]

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

Goal state before:
pp: b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ log (-b) < 0

Tactic:
log_neg_iff (by linarith)

Goal state after:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ -b < 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case mp
x a : ℝ
⊢ 0 ^ x = a → x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
intro hyp

Goal state after:
case mp
x a : ℝ
hyp : 0 ^ x = a
⊢ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ x ^ y * x ^ z ≤ x ^ (y + z)

Tactic:
rcases le_iff_eq_or_lt.1 hx with (H | pos)
  · by_cases h : y + z = 0
    · simp only [H.symm, h, rpow_zero]
      calc
        (0 : ℝ) ^ y * 0 ^ z ≤ 1 * 1 := by
          gcongr
          exacts [zero_rpow_nonneg z, zero_rpow_le_one y, zero_rpow_le_one z]
        _ = 1 := by simp
    · simp [rpow_add', ← H, h]
  · simp [rpow_add pos]

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

Goal state before:
pp: case inr
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 < x
⊢ log x * z < log y * z

Tactic:
exact mul_lt_mul_of_pos_right (log_lt_log hx hxy) hz

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

Goal state before:
pp: case refine_2
z✝ : ℂ
hz✝ : 0 < z✝.re
hz₀ : z✝ ≠ 0
C : ℝ
hC : |z✝.im| < C
z : ℂ × ℂ
hz : |(im ∘ Prod.snd) z| < C
⊢ |z.1.arg * z.2.im| ≤ π * C

Tactic:
_root_.abs_mul

Goal state after:
case refine_2
z✝ : ℂ
hz✝ : 0 < z✝.re
hz₀ : z✝ ≠ 0
C : ℝ
hC : |z✝.im| < C
z : ℂ × ℂ
hz : |(im ∘ Prod.snd) z| < C
⊢ |z.1.arg| * |z.2.im| ≤ π * C
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x z : ℝ
hx : 1 < x
hz : 0 < z
⊢ 1 ^ z < x ^ z

Tactic:
exact rpow_lt_rpow zero_le_one hx hz

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

Goal state before:
pp: case inr.inr.coe.coe
z : ℝ
hz : z < 0 ∨ 0 < z
x✝¹ : ℝ≥0
hx0 : ↑x✝¹ ≠ 0
x✝ : ℝ≥0
hy0 : ↑x✝ ≠ 0
hxy : ↑x✝¹ ≤ ↑x✝
⊢ (↑x✝¹ * ↑x✝) ^ z = if (False ∧ ↑x✝ = ∞ ∨ ↑x✝¹ = ∞ ∧ False) ∧ z < 0 then ∞ else ↑x✝¹ ^ z * ↑x✝ ^ z

Tactic:
norm_cast at *

Goal state after:
case inr.inr.coe.coe
z : ℝ
x✝¹ x✝ : ℝ≥0
hz : z < 0 ∨ 0 < z
hx0 : ¬x✝¹ = 0
hy0 : ¬x✝ = 0
hxy : x✝¹ ≤ x✝
⊢ ↑(x✝¹ * x✝) ^ z = if (False ∧ ↑x✝ = ∞ ∨ ↑x✝¹ = ∞ ∧ False) ∧ z < 0 then ∞ else ↑x✝¹ ^ z * ↑x✝ ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x < y ^ z⁻¹ ↔ x ^ z < y

Tactic:
nth_rw 1 [← rpow_one x]
  nth_rw 1 [← @mul_inv_cancel₀ _ _ z (ne_of_lt hz).symm]
  rw [rpow_mul, @rpow_lt_rpow_iff _ _ z⁻¹ (by simp [hz])]

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

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

Tactic:
← ENNReal.rpow_one y

Goal state after:
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ z⁻¹ ≤ y ^ 1 ↔ x ≤ y ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ x ^ y < x ^ z

Tactic:
lift x to ℝ≥0 using ne_of_lt (lt_of_lt_of_le hx1 le_top)

Goal state after:
y z : ℝ
hyz : z < y
x : ℝ≥0
hx0 : 0 < ↑x
hx1 : ↑x < 1
⊢ ↑x ^ y < ↑x ^ z
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x r : ℝ
hx : 0 ≤ x
⊢ x ^ (r / 2) = √x ^ r

Tactic:
by
  rw [sqrt_eq_rpow, ← rpow_mul hx]
  congr
  ring

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

Goal state before:
pp: x : ℝ≥0∞
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
⊢ x ^ z ≤ x

Tactic:
← ENNReal.rpow_one x

Goal state after:
x : ℝ≥0∞
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
⊢ x ^ z ≤ x ^ 1
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
⊢ x ^ z ≤ x ^ 1

Tactic:
exact ENNReal.rpow_le_rpow_of_exponent_ge hx h_one_le

Goal state after: