mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : PartialHomeomorph X Y
f : PartialEquiv X Y
h : IsHomeomorph ⇑f.toEquiv
⊢ ContinuousOn f.invFun f.target

Tactic:
rw [continuousOn_iff_continuous_domRestrict,
      ← continuous_codRestrict_iff (s := f.source) (by simp)]

Goal state after:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : PartialHomeomorph X Y
f : PartialEquiv X Y
h : IsHomeomorph ⇑f.toEquiv
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype]
    (codRestrict (f.target.domRestrict f.invFun) f.source ⋯)
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : Norm E
inst✝³ : Norm F
f : α → E
inst✝² : One F
inst✝¹ : NormOneClass F
inst✝ : TopologicalSpace α
a : α
c : ℝ
hc : ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ c
b : α
hb : b ∈ {a}ᶜ → ‖f b‖ ≤ c
⊢ ‖f b‖ ≤ max c ‖f a‖

Tactic:
rcases eq_or_ne b a with rfl | hb'

Goal state after:
case inl
α : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : Norm E
inst✝³ : Norm F
f : α → E
inst✝² : One F
inst✝¹ : NormOneClass F
inst✝ : TopologicalSpace α
c : ℝ
b : α
hc : ∀ᶠ (a : α) in 𝓝[≠] b, ‖f a‖ ≤ c
hb : b ∈ {b}ᶜ → ‖f b‖ ≤ c
⊢ ‖f b‖ ≤ max c ‖f b‖

case inr
α : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : Norm E
inst✝³ : Norm F
f : α → E
inst✝² : One F
inst✝¹ : NormOneClass F
inst✝ : TopologicalSpace α
a : α
c : ℝ
hc : ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ c
b : α
hb : b ∈ {a}ᶜ → ‖f b‖ ≤ c
hb' : b ≠ a
⊢ ‖f b‖ ≤ max c ‖f a‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case inl
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
B : ι → α → ℝ
hAB : ∀ i ∈ ∅, IsBigOWith (C i) l (A i) (B i)
⊢ IsBigOWith (sSup (C '' ↑∅)) l (fun H ↦ ∑ i ∈ ∅, A i H) fun H ↦ ∑ i ∈ ∅, ‖B i H‖

Tactic:
simp [isBigOWith_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
h₂ : (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k
h₃ :
  ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k
two_mul_two : 4 = 2 * 2
h : Q = 0
⊢ False

Tactic:
by simp [h] at hQε0

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

Goal state before:
pp: x : ℝ
⊢ (starRingEnd ℂ) (cosh ↑x) = cosh ↑x

Tactic:
by rw [← cosh_conj, conj_ofReal]

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

Goal state before:
pp: z : ℂ
⊢ sin z = sin ↑z.re * cosh ↑z.im + cos ↑z.re * sinh ↑z.im * I

Tactic:
by
  convert! sin_add_mul_I z.re z.im; exact (re_add_im z).symm

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

Goal state before:
pp: x y : ℂ
⊢ cos (x + y * I) = cos x * cosh y - sin x * sinh y * I

Tactic:
by
  rw [cos_add, cos_mul_I, sin_mul_I, mul_assoc]

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

Goal state before:
pp: E : Type u_3
E'' : Type u_9
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup E''
f : ℕ → E
g'' : ℕ → E''
h : f =O[atTop] g''
⊢ f =O[cofinite] g''

Tactic:
rwa [Nat.cofinite_eq_atTop]

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
hx' : x < 2
⊢ rexp x ≤ (2 + x) / (2 - x)

Tactic:
by
  obtain rfl | hx₀ := hx.eq_or_lt
  · simp
  · exact (exp_lt_two_add_div_two_sub hx₀ hx').le

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
⊢ ∀ n ≥ 0, |(1 - abv x ^ n) / (1 - abv x)| ≤ 1 / (1 - abv x)

Tactic:
intro n _
    rw [abs_of_nonneg]
    · gcongr
      exact sub_le_self _ (abv_pow abv x n ▸ abv_nonneg _ _)
    refine div_nonneg (sub_nonneg.2 ?_) (sub_nonneg.2 <| le_of_lt hx1)
    exact pow_le_one₀ (by positivity) hx1.le

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:
tendsto_Ioi_atTop

Goal state after:
α : Type u_1
x y z : ℝ
l : Filter α
⊢ Tendsto (fun x ↦ ↑⟨rexp x, ⋯⟩) atTop atTop
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: a : ℝ
⊢ Subtype.val '' ⇑expOrderIso '' Set.Iio a = Set.Ioo 0 ((Subtype.val ∘ ⇑expOrderIso) a)

Tactic:
expOrderIso.image_Iio,

Goal state after:
a : ℝ
⊢ Subtype.val '' Set.Iio (expOrderIso a) = Set.Ioo 0 ((Subtype.val ∘ ⇑expOrderIso) a)
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : r ≠ 0
⊢ interior (closedBall x r) = ball x r

Tactic:
exact interior_closedBall x hr

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

Goal state before:
pp: θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ 2 * s * c = sin (2 * θ)

Tactic:
sin_two_mul

Goal state after:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ 2 * s * c = 2 * sin θ * cos θ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ sin (2 * θ) * c + cos (2 * θ) * s = 2 * s * c * c + cos (2 * θ) * s

Tactic:
sin_two_mul

Goal state after:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
hs : s ≠ 0
⊢ 2 * sin θ * cos θ * c + cos (2 * θ) * s = 2 * s * c * c + cos (2 * θ) * s
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ tan (π / 3) = √3

Tactic:
rw [tan_eq_sin_div_cos, sin_pi_div_three, cos_pi_div_three]
  ring

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

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 ≤ δ
x : E
⊢ thickening ε (Metric.closedBall x δ) = Metric.ball x (ε + δ)

Tactic:
by
  rw [← cthickening_singleton _ hδ, thickening_cthickening hε hδ, thickening_singleton]

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

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
a b : E
⊢ Metric.ball (a + b) (δ + ε) = Metric.ball (a + b) (ε + δ)

Tactic:
add_comm δ

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
a b : E
⊢ Metric.ball (a + b) (ε + δ) = Metric.ball (a + b) (ε + δ)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
δ ε : ℝ
inst✝ : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.closedBall (a + b) (δ + ε) = Metric.closedBall (a + b) (ε + δ)

Tactic:
add_comm δ

Goal state after:
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
δ ε : ℝ
inst✝ : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.closedBall (a + b) (ε + δ) = Metric.closedBall (a + b) (ε + δ)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ HasSum (fun n ↦ ↑n * x ^ n) (x * (1 - x)⁻¹ʳ ^ 2)

Tactic:
have A : HasSum (fun (n : ℕ) ↦ (n + 1) * x ^ n) ((1 - x)⁻¹ʳ ^ 2) := by
    convert! hasSum_choose_mul_geometric_of_norm_lt_one' 1 h with n
    simp

Goal state after:
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n ↦ (↑n + 1) * x ^ n) ((1 - x)⁻¹ʳ ^ 2)
⊢ HasSum (fun n ↦ ↑n * x ^ n) (x * (1 - x)⁻¹ʳ ^ 2)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hr : r < 1
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
a : α
ha : HasSum f a
n : ℕ
⊢ dist (∑ x ∈ Finset.range n, f x) a ≤ C * r ^ n / (1 - r)

Tactic:
apply dist_le_of_le_geometric_of_tendsto r C hr (dist_partial_sum_le_of_le_geometric hf)

Goal state after:
α : Type u_1
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hr : r < 1
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
a : α
ha : HasSum f a
n : ℕ
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 a)
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
⊢ JoinedIn F y x

Tactic:
obtain ⟨hx, hy⟩ := h.mem

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
hx : x ∈ F
hy : y ∈ F
⊢ JoinedIn F y x
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∃ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), N₀ ≤ b → r * ‖f b‖ ≤ ‖f (b + 1)‖
⊢ ¬Summable f

Tactic:
frequently_atTop

Goal state after:
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
r : ℝ
hr : 1 < r
hf : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ‖f b‖ ≠ 0
N₀ : ℕ
hN₀ : ∀ (b : ℕ), N₀ ≤ b → r * ‖f b‖ ≤ ‖f (b + 1)‖
⊢ ¬Summable f
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
⊢ ⇑(γ₁.trans γ₂).extend '' Iic (1 / 2) ∪ ⇑(γ₁.trans γ₂).extend '' Ici (1 / 2) = range ⇑γ₁ ∪ range ⇑γ₂

Tactic:
EqOn.image_eq fun t ht ↦ extend_trans_of_le_half _ _ (mem_Iic.1 ht),

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
⊢ (fun t ↦ γ₁.extend (2 * t)) '' Iic (1 / 2) ∪ ⇑(γ₁.trans γ₂).extend '' Ici (1 / 2) = range ⇑γ₁ ∪ range ⇑γ₂
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr
p x ε : ℝ
hp : p ≠ 0
y : ℝ
n : ℤ
hn : |p⁻¹ * (y - x) - p⁻¹ * (↑n * p)| ≤ |p⁻¹| * ε
⊢ |p⁻¹ * (y - x) - p⁻¹ * (↑(round (p⁻¹ * (y - x))) * p)| ≤ |p⁻¹| * ε

Tactic:
mul_comm _ p,

Goal state after:
case inr
p x ε : ℝ
hp : p ≠ 0
y : ℝ
n : ℤ
hn : |p⁻¹ * (y - x) - p⁻¹ * (p * ↑n)| ≤ |p⁻¹| * ε
⊢ |p⁻¹ * (y - x) - p⁻¹ * (p * ↑(round (p⁻¹ * (y - x))))| ≤ |p⁻¹| * ε
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:
by
  ext x
  rw [cast_coe]
  have : ↑x ∈ (Icc 0 1 : Set ℝ) := x.2
  rw [truncate, coe_mk_mk, max_eq_left this.1, min_eq_left this.2, extend_extends']

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

Goal state before:
pp: case inr.inr.inl.inl
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : 0 < p
hz' : ↑z ≤ -1
⊢ False

Tactic:
have : ↑z * p ≤ -p := by nlinarith
        linarith [abs_eq_self.mpr hp.le]

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

Goal state before:
pp: case inr.inr.inr.inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
hz' : 1 ≤ ↑z
⊢ False

Tactic:
have : ↑z * p ≤ p := by nlinarith

Goal state after:
case inr.inr.inr.inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
hz' : 1 ≤ ↑z
this : ↑z * p ≤ p
⊢ False
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p : ℝ
hp : Fact (0 < p)
m n : ℕ
⊢ p⁻¹ * (↑m / ↑n * p) = ↑m / ↑n

Tactic:
mul_comm _ p,

Goal state after:
p : ℝ
hp : Fact (0 < p)
m n : ℕ
⊢ p⁻¹ * (p * (↑m / ↑n)) = ↑m / ↑n
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
⊢ ∃ k, ‖u‖ = p * (↑k / ↑n)

Tactic:
obtain ⟨m, -, -, hm⟩ := exists_gcd_eq_one_of_isOfFinAddOrder hu

Goal state after:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
m : ℕ
hm : ↑(↑m / ↑(addOrderOf u) * p) = u
⊢ ∃ k, ‖u‖ = p * (↑k / ↑n)
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
⊢ p * 1 ≤ ↑(addOrderOf u) * p * (↑n / ↑(addOrderOf u))

Tactic:
mul_comm _ p,

Goal state after:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
⊢ p * 1 ≤ p * ↑(addOrderOf u) * (↑n / ↑(addOrderOf u))
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ z.arg = 0 ↔ 0 ≤ z

Tactic:
rw [arg_eq_zero_iff, eq_comm, nonneg_iff]

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

Goal state before:
pp: R : Type u_4
K : Type u_5
inst✝⁹ : NormedRing K
inst✝⁸ : NormedRing R
inst✝⁷ : Module K R
inst✝⁶ : IsTorsionFree K R
inst✝⁵ : NormSMulClass K R
inst✝⁴ : NormSMulClass ℤ K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorSemiring K
inst✝ : HasSolidNorm K
g : ℕ → R
t : R
hg : Tendsto (fun n ↦ ↑n * g n) atTop (𝓝 t)
⊢ Tendsto (fun n ↦ n • g n) atTop (𝓝 t)

Tactic:
by simpa only [nsmul_eq_mul] using hg

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

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

Tactic:
arg_ofReal_of_nonneg hx

Goal state after:
x : ℝ
hx : 0 ≤ x
⊢ 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
⊢ ↑(Real.log ‖x‖) + ↑((starRingEnd ℂ) x).arg * I =
    if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I else (starRingEnd ℂ) (↑(Real.log ‖x‖) + ↑x.arg * I)

Tactic:
arg_conj,

Goal state after:
x : ℂ
⊢ ↑(Real.log ‖x‖) + ↑(if x.arg = π then π else -x.arg) * I =
    if x.arg = π then ↑(Real.log ‖x‖) + ↑x.arg * I else (starRingEnd ℂ) (↑(Real.log ‖x‖) + ↑x.arg * I)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
hx : 0 ≤ x.im
x✝ : ∃ n, x = ↑n * (2 * ↑π * I)
n : ℕ
hn : x = ↑↑n * (2 * ↑π * I)
this : 0 ≤ ↑↑n * (2 * π)
⊢ ∃ n, x = ↑n * (2 * ↑π * I)

Tactic:
exact ⟨n, hn⟩

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

Goal state before:
pp: case mp.inl
θ ψ : ℝ
n : ℤ
hn : ↑n * π = (θ + ψ) / 2
⊢ ↑θ = -↑ψ

Tactic:
rw [eq_div_iff_mul_eq (two_ne_zero' ℝ), ← sub_eq_iff_eq_add] at hn

Goal state after:
case mp.inl
θ ψ : ℝ
n : ℤ
hn : ↑n * π * 2 - ψ = θ
⊢ ↑θ = -↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp
θ ψ : ℝ
Hsin : sin θ = sin ψ
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π

Tactic:
rw [← cos_pi_div_two_sub, ← cos_pi_div_two_sub] at Hsin

Goal state after:
case mp
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = -↑ψ
⊢ ↑θ = ↑ψ

Tactic:
rcases sin_eq_iff_coe_eq_or_add_eq_pi.mp Hsin with hs | hs

Goal state after:
case inr.inl
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = -↑ψ
hs : ↑θ = ↑ψ
⊢ ↑θ = ↑ψ

case inr.inr
θ ψ : ℝ
Hcos : cos θ = cos ψ
Hsin : sin θ = sin ψ
hc : ↑θ = -↑ψ
hs : ↑θ + ↑ψ = ↑π
⊢ ↑θ = ↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inl
z : ℂ
hre : z.re < 0
this : z ≠ 0
⊢ (0 ≤ z.re ∨ z.im < 0) ∧ ¬(z.re = 0 ∧ 0 < z.im) ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0

Tactic:
simp [hre.ne, hre.not_ge, hre.not_gt, this]

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

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

Tactic:
induction θ using Real.Angle.induction_on
  exact Real.cos_sq_add_sin_sq _

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

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

Tactic:
rw [← toReal_inj, toReal_pi]

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

Goal state before:
pp: θ : ℝ
⊢ (cos ↑θ + sin ↑θ * I).arg = toIocMod Real.two_pi_pos (-π) θ

Tactic:
rw [← one_mul (_ + _), ← ofReal_one, arg_mul_cos_add_sin_mul_I_eq_toIocMod zero_lt_one]

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

Goal state before:
pp: case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
ha : Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z ↦ ↑z.arg + ↑π
⊢ ContinuousAt (Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π) (-x)

Tactic:
ha

Goal state after:
case neg
x : ℂ
h : x ≠ 0
hs : x ∉ slitPlane
ha : Function.update ((Real.Angle.coe ∘ arg) ∘ Neg.neg) 0 ↑π = fun z ↦ ↑z.arg + ↑π
⊢ ContinuousAt (fun z ↦ ↑z.arg + ↑π) (-x)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
split_ifs with h <;> simp [rpow_def, *]; exact rpow_def_of_neg (lt_of_le_of_ne hx h) _

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

Goal state before:
pp: case inr
x y : ℝ
hx : x < 0
⊢ |x ^ y| ≤ (-x) ^ y

Tactic:
rpow_def_of_neg hx,

Goal state after:
case inr
x y : ℝ
hx : x < 0
⊢ |rexp (log x * y) * cos (y * π)| ≤ (-x) ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: case h
y : ℝ
hy : 0 < y
b : ℝ≥0
c : ℝ
hc : ∀ (a : ℝ), c ≤ a → ↑b ≤ a ^ y
a : ℝ≥0
⊢ c.toNNReal ≤ a → b ≤ a ^ y

Tactic:
ha

Goal state after:
case h
y : ℝ
hy : 0 < y
b : ℝ≥0
c : ℝ
hc : ∀ (a : ℝ), c ≤ a → ↑b ≤ a ^ y
a : ℝ≥0
ha : c.toNNReal ≤ a
⊢ b ≤ a ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

Goal state before:
pp: y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
hc' : Set.Ioi ↑c ∈ 𝓝 ∞
a : ℝ≥0∞
⊢ a ∈ Set.Ioi ↑c → ↑x < a ^ y

Tactic:
ha

Goal state after:
y : ℝ
hy : 0 < y
x c : ℝ≥0
left✝ : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
hc' : Set.Ioi ↑c ∈ 𝓝 ∞
a : ℝ≥0∞
ha : a ∈ Set.Ioi ↑c
⊢ ↑x < a ^ y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

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

Tactic:
by
  rw [rpow_add' hx h, rpow_natCast]

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

Goal state before:
pp: case inr.inr
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_neg : p < 0
⊢ 0 < (x ^ (-p))⁻¹

Tactic:
inv_pos

Goal state after:
case inr.inr
p : ℝ
x : ℝ≥0
hx_pos : 0 < x
rpow_pos_of_nonneg : ∀ {p : ℝ}, 0 < p → 0 < x ^ p
hp_neg : p < 0
⊢ 0 < x ^ (-p)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

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

Tactic:
exact A.comp_of_eq B rfl

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

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
⊢ x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y

Tactic:
rcases hx.eq_or_lt with (rfl | hx)
  · rcases _root_.em (y = 0) with (rfl | hy) <;> simp [*, zero_lt_one]
  · simp [rpow_lt_one_iff_of_pos hx, hx.ne.symm]

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

Goal state before:
pp: x y z : ℝ
hx : 0 < x
hy : 0 < y
⊢ x < y ^ z ↔ log x < z * log y

Tactic:
rw [← log_lt_log_iff hx (rpow_pos_of_pos hy z), log_rpow hy]

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

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

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp
  | insert _ _ hi ih => simp_rw [prod_insert hi, ih, ← coe_mul_rpow, coe_mul]

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

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

Tactic:
cases x
  · rcases lt_trichotomy y 0 with (Hy | Hy | Hy) <;>
    rcases lt_trichotomy z 0 with (Hz | Hz | Hz) <;>
    simp [Hy, Hz, top_rpow_of_neg, top_rpow_of_pos] <;>
    linarith
  · simp only [one_le_coe_iff] at hx
    simp [← coe_rpow_of_ne_zero (ne_of_gt (lt_of_lt_of_le zero_lt_one hx)),
      NNReal.rpow_le_rpow_of_exponent_le hx hyz]

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

Goal state before:
pp: case coe
z : ℝ
hz : 0 < z
x✝ : ℝ≥0
hx : 1 < x✝
⊢ 1 < ↑x✝ ^ z

Tactic:
simp [← coe_rpow_of_nonneg _ (le_of_lt hz), NNReal.one_lt_rpow hx hz]

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

Goal state before:
pp: a b : ℝ
n d : ℕ
hb : IsRat b (Int.negOfNat n) d
⊢ a ^ b = a⁻¹ ^ (↑n / ↑d)

Tactic:
by
  rw [← Real.rpow_neg_eq_inv_rpow, hb.neg_to_eq rfl rfl]

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:
by
  rw [midpoint_comm]; simp

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : Invertible 2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
inst✝³ : Ring R'
inst✝² : Invertible 2
inst✝¹ : AddCommGroup F
inst✝ : Module R' F
f : E → F
h0 : f 0 = 0
hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)
x y : E
⊢ f (x + y) = f 0 + f (x + y)

Tactic:
rw [h0, zero_add]

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

Goal state before:
pp: k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
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
inst✝⁵ : AddCommGroup V3
inst✝⁴ : Module k V3
inst✝³ : AffineSpace V3 P3
inst✝² : AddCommGroup V4
inst✝¹ : Module k V4
inst✝ : AffineSpace V4 P4
f : P2 →ᵃ[k] P3
g : P1 →ᵃ[k] P2
⊢ ∀ (p : P1) (v : V1), (⇑f ∘ ⇑g) (v +ᵥ p) = (f.linear ∘ₗ g.linear) v +ᵥ (⇑f ∘ ⇑g) p

Tactic:
intro p v
    rw [Function.comp_apply, g.map_vadd, f.map_vadd]
    rfl

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddRightMono 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
a b : E
x : F
⊢ x ∈ ⇑f '' ⇑(AffineMap.lineMap a b) '' Icc 0 1 ↔ x ∈ ⇑(AffineMap.lineMap (f a) (f b)) '' Icc 0 1

Tactic:
mem_image,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : Ring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddRightMono 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
a b : E
x : F
⊢ (∃ x_1, (∃ x ∈ Icc 0 1, (AffineMap.lineMap a b) x = x_1) ∧ f x_1 = x) ↔
    ∃ x_1 ∈ Icc 0 1, (AffineMap.lineMap (f a) (f b)) x_1 = x