mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ∑ 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

Tactic:
rw [← sum_add_distrib]

Goal state after:
α : 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
⊢ ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ x ∈ range K, (f x * (∑ k ∈ range (K - x), g k - ∑ k ∈ range K, g k) + f x * ∑ k ∈ range K, g k)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : cos x ≠ 0
⊢ (1 + (sin x / cos x) ^ 2)⁻¹ = cos x ^ 2

Tactic:
div_pow

Goal state after:
x : ℂ
hx : cos x ≠ 0
⊢ (1 + sin x ^ 2 / cos x ^ 2)⁻¹ = cos x ^ 2
Module: Mathlib.Analysis.Asymptotics.Lemmas

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

Tactic:
by
  rw [isBigO_iff_isBigOWith, isBigO_iff_isBigOWith]
  simp [isBigOWith_mul_iff_isBigOWith_div hf]

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

Goal state before:
pp: n : ℕ
x a₁ b₁ : ℝ
m : ℕ
e₁ : n + 1 = m
a₂ b₂ : ℝ
e : |1 + x / ↑m * a₂ - a₁| ≤ b₁ - |x| / ↑m * b₂
h : |rexp x - expNear m x a₂| ≤ |x| ^ m / ↑m.factorial * b₂
⊢ |x| ^ m / ↑m.factorial * b₂ + |expNear m x a₂ - expNear n x a₁| ≤ |x| ^ n / ↑n.factorial * b₁

Tactic:
subst e₁

Goal state after:
n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : |1 + x / ↑(n + 1) * a₂ - a₁| ≤ b₁ - |x| / ↑(n + 1) * b₂
h : |rexp x - expNear (n + 1) x a₂| ≤ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂
⊢ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂ + |expNear (n + 1) x a₂ - expNear n x a₁| ≤ |x| ^ n / ↑n.factorial * b₁
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
hg : Summable fun x ↦ ‖g x‖
⊢ HasSum (fun n ↦ ∑ k ∈ range (n + 1), f k * g (n - k)) ((∑' (n : ℕ), f n) * ∑' (n : ℕ), g n)

Tactic:
convert! (summable_norm_sum_mul_range_of_summable_norm hf hg).of_norm.hasSum

Goal state after:
case e'_6
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
hg : Summable fun x ↦ ‖g x‖
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (b : ℕ), ∑ k ∈ range (b + 1), f k * g (b - k)
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case refine_2
α : 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 : ℕ
a✝ : n ≥ 0
⊢ (1 - abv x ^ n) / (1 - abv x) ≤ (1 - abv x ^ n.succ) / (1 - abv x)

Tactic:
rw [← one_mul (abv x ^ n), pow_succ']

Goal state after:
case refine_2
α : 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 : ℕ
a✝ : n ≥ 0
⊢ (1 - 1 * abv x ^ n) / (1 - abv x) ≤ (1 - abv x * abv x ^ n) / (1 - abv x)
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
⊢ Tendsto (fun x ↦ x ^ n / (b * rexp x + c)) atTop (𝓝 0)

Tactic:
rcases lt_or_gt_of_ne hb with h | h

Goal state after:
case inl
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : 0 < b
⊢ Tendsto (fun x ↦ x ^ n / (b * rexp x + c)) atTop (𝓝 0)

case inr
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : b < 0
⊢ Tendsto (fun x ↦ x ^ n / (b * rexp x + c)) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: k : ℕ
r : ℝ
hr : 0 < r
⊢ Summable fun n ↦ ↑n ^ k * rexp (↑n * -r)

Tactic:
exp_nat_mul

Goal state after:
k : ℕ
r : ℝ
hr : 0 < r
⊢ Summable fun n ↦ ↑n ^ k * rexp (-r) ^ n
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
this : ∀ (ε : ℝ), mk '' ball 1 ε = {x | ‖x‖ < ε}
⊢ (𝓝 1).HasBasis (fun ε ↦ 0 < ε) fun ε ↦ {x | ‖x‖ < ε}

Tactic:
rw [← mk_one, nhds_eq, ← funext this]

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
this : ∀ (ε : ℝ), mk '' ball 1 ε = {x | ‖x‖ < ε}
⊢ (Filter.map mk (𝓝 1)).HasBasis (fun ε ↦ 0 < ε) fun x ↦ mk '' ball 1 x
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x✝ : M ⧸ S
m : M
r✝ ε : ℝ
h : S ≤ T
x : (M ⧸ S) ⧸ Subgroup.map (mk' S) T
r : ℝ
h₁ : ∀ (m : M), ↑m = (quotientQuotientEquivQuotient S T h) x → r ≤ ‖m‖
y : M ⧸ S
h₂ : ↑y = x
z : M
h₃ : ↑z = y
⊢ ↑z = (quotientQuotientEquivQuotient S T h) x

Tactic:
subst_vars

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r✝ ε : ℝ
h : S ≤ T
r : ℝ
z : M
h₁ : ∀ (m : M), ↑m = (quotientQuotientEquivQuotient S T h) ↑↑z → r ≤ ‖m‖
⊢ ↑z = (quotientQuotientEquivQuotient S T h) ↑↑z
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
⊢ c • ball x r = ball (c • x) (‖c‖ * r)

Tactic:
ext y

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ y ∈ c • ball x r ↔ y ∈ ball (c • x) (‖c‖ * r)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
⊢ c • sphere x r = sphere (c • x) (‖c‖ * r)

Tactic:
ext y

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ y ∈ c • sphere x r ↔ y ∈ sphere (c • x) (‖c‖ * r)
Module: Mathlib.Topology.Hom.ContinuousEval

Goal state before:
pp: F : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁶ : FunLike F X Y
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : ContinuousEval F X Y
F' : Type u_5
inst✝¹ : FunLike F' X Y
inst✝ : TopologicalSpace F'
f : F' → F
hc : Continuous[inst✝, inst✝⁵] f
hf : ∀ (g : F'), ⇑(f g) = ⇑g
⊢ Continuous[instTopologicalSpaceProd, inst✝³] fun fx ↦ fx.1 fx.2

Tactic:
by simpa only [← hf] using hc.fst'.eval continuous_snd

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

Goal state before:
pp: K : Type u_4
inst✝ : NormedDivisionRing K
ξ : K
h : ‖ξ‖ < 1
xi_ne_one : ξ ≠ 1
A : Tendsto (fun n ↦ (ξ ^ n - 1) * (ξ - 1)⁻¹) atTop (𝓝 ((0 - 1) * (ξ - 1)⁻¹))
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, ξ ^ i) atTop (𝓝 (1 - ξ)⁻¹)

Tactic:
simpa [geom_sum_eq, xi_ne_one, neg_inv, div_eq_mul_inv] using A

Goal state after:
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
⊢ x ∈ F ∧ y ∈ F

Tactic:
by
  rcases h with ⟨γ, γ_in⟩
  have : γ 0 ∈ F ∧ γ 1 ∈ F := by constructor <;> apply γ_in
  simpa using this

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case right
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
⊢ pathComponentIn F x = F

Tactic:
ext y

Goal state after:
case right
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
y : X
⊢ y ∈ pathComponentIn F x ↔ y ∈ F
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: ι : Type u_3
Z : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (Z i)
x : (i : ι) → Z i
⊢ pathComponent x = univ.pi fun i ↦ pathComponent (x i)

Tactic:
ext y

Goal state after:
ι : Type u_3
Z : ι → Type u_4
inst✝ : (i : ι) → TopologicalSpace (Z i)
x y : (i : ι) → Z i
⊢ y ∈ pathComponent x ↔ y ∈ univ.pi fun i ↦ pathComponent (x i)
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
T : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace T
t : Set X
f : T → X → Y
g : C(↑t, Y)
f_cont : ContinuousOn (Function.uncurry f) (univ ×ˢ t)
⊢ Continuous[inst✝, _] fun x ↦ mkD (t.domRestrict (f x)) g

Tactic:
by
  have (x : _) : ContinuousOn (f x) t :=
    f_cont.comp (Continuous.prodMk_right x).continuousOn fun _ hz ↦ ⟨trivial, hz⟩
  refine continuous_of_continuous_uncurry _ ?_
  conv in mkD _ _ => rw [mkD_of_continuousOn (this x)]
  exact f_cont.comp_continuous (.prodMap continuous_id continuous_subtype_val)
    fun xz ↦ ⟨trivial, xz.2.2⟩

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ mk ⁻¹' {mk x} = pathComponent x

Tactic:
ext y

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ y ∈ mk ⁻¹' {mk x} ↔ y ∈ pathComponent x
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y x' y' : X
hx : x' = x
hy : y' = y
⊢ Bijective fun x_1 ↦ x_1.cast hx hy

Tactic:
subst_vars

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x' y' : X
⊢ Bijective fun x ↦ x.cast ⋯ ⋯
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case e_s
p x t : ℝ
ht : t ≠ 0
m : ℝ
⊢ m ∈ {m | ↑m = ↑(t * x)} ↔ m ∈ t • {m | ↑m = ↑x}

Tactic:
zmultiples,

Goal state after:
case e_s
p x t : ℝ
ht : t ≠ 0
m : ℝ
⊢ m ∈ {m | ↑m = ↑(t * x)} ↔ m ∈ t • {m | ↑m = ↑x}
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: x : ℝ
⊢ {y | ↑y = ↑x} = {x}

Tactic:
ext y

Goal state after:
x y : ℝ
⊢ y ∈ {y | ↑y = ↑x} ↔ y ∈ {x}
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
⊢ ‖↑x‖ = |x - ↑(round (p⁻¹ * x)) * p|

Tactic:
rcases eq_or_ne p 0 with (rfl | hp)
    · simp
    have hx := norm_coe_mul p x p⁻¹
    rw [abs_inv, eq_inv_mul_iff_mul_eq₀ ((not_congr abs_eq_zero).mpr hp)] at hx
    rw [← hx, inv_mul_cancel₀ hp, this, ← abs_mul, mul_sub, mul_inv_cancel_left₀ hp, mul_comm p]

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

Goal state before:
pp: case inr.left
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
⊢ -(1 / 2) ≤ p⁻¹ * x

pp: case inr.right
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
⊢ p⁻¹ * x < 1 / 2

Tactic:
· rwa [le_inv_mul_iff₀ hp, mul_neg, ← mul_div_assoc, mul_one]

Goal state after:
case inr.right
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
⊢ p⁻¹ * x < 1 / 2
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: x ε : ℝ
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε = closedBall x ε

Tactic:
ext y

Goal state after:
x ε y : ℝ
⊢ y ∈ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ↔ y ∈ closedBall x ε
Module: Mathlib.Analysis.Normed.Group.AddCircle

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

Tactic:
ext y

Goal state after:
case inr
p x ε : ℝ
hp : p ≠ 0
y : ℝ
⊢ y ∈ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ↔ y ∈ ⋃ z, closedBall (x + z • p) ε
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
⊢ ‖x‖ * Real.cos x.arg = x.re

Tactic:
by
  simpa [-norm_mul_cos_add_sin_mul_I] using! congr_arg re (norm_mul_cos_add_sin_mul_I x)

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

Goal state before:
pp: case inl
hπ : 0 < π
⊢ arg 0 ∈ Ioc (-π) π

Tactic:
simp [hπ, hπ.le]

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

Goal state before:
pp: R : Type u_4
K : Type u_5
inst✝¹⁰ : NormedRing K
inst✝⁹ : IsDomain K
inst✝⁸ : NormedAddCommGroup 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 x ↦ x • g ⌊x⌋₊) atTop (𝓝 t)

Tactic:
replace hg : Tendsto (fun n : ℕ ↦ (n : K) • g n) atTop (𝓝 t) := mod_cast hg

Goal state after:
R : Type u_4
K : Type u_5
inst✝¹⁰ : NormedRing K
inst✝⁹ : IsDomain K
inst✝⁸ : NormedAddCommGroup 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 x ↦ x • g ⌊x⌋₊) atTop (𝓝 t)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
h₁ : 0 ≤ z.im
h₂ : z ≠ 0
⊢ z.arg = Real.arccos (z.re / ‖z‖)

Tactic:
by
  rw [← cos_arg h₂, Real.arccos_cos (arg_nonneg_iff.2 h₁) (arg_le_pi _)]

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

Goal state before:
pp: ⊢ Tendsto log (𝓝[>] 0) atBot

Tactic:
simpa [← tendsto_comp_exp_atBot] using! tendsto_id

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

Goal state before:
pp: x : ℂ
hx : x = 0
⊢ x ^ 1 = x

Tactic:
simp [hx, cpow_def]

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

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

Tactic:
by
  rw [cpow_def]
  split_ifs <;> simp_all [one_ne_zero]

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

Goal state before:
pp: z : ℂ
⊢ |z.arg| < π / 2 ↔ 0 < z.re ∨ z = 0

Tactic:
rw [abs_lt, arg_lt_pi_div_two_iff, neg_pi_div_two_lt_arg_iff, ← or_and_left]
  rcases eq_or_ne z 0 with hz | hz
  · simp [hz]
  · simp_rw [hz, or_false, ← not_lt, not_and_self_iff, or_false]

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

Goal state before:
pp: θ ψ : ℝ
⊢ ↑(toIcoMod two_pi_pos ψ θ) = ↑θ

Tactic:
rw [angle_eq_iff_two_pi_dvd_sub]
  refine ⟨-toIcoDiv two_pi_pos ψ θ, ?_⟩
  rw [toIcoMod_sub_self, zsmul_eq_mul, mul_comm]

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

Goal state before:
pp: z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : 0 ≤ a✝.im
hre : a✝.re < 0
⊢ (if 0 ≤ a✝.im then Real.arcsin ((-a✝).im / ‖a✝‖) + π else Real.arcsin ((-a✝).im / ‖a✝‖) - π) =
    Real.arcsin ((-a✝).im / ‖a✝‖) + π

Tactic:
if_pos him

Goal state after:
z : ℂ
hre✝ : z.re < 0
him✝ : z.im = 0
this : ∀ᶠ (x : ℂ) in 𝓝 z, x.re < 0
a✝ : ℂ
him : 0 ≤ a✝.im
hre : a✝.re < 0
⊢ Real.arcsin ((-a✝).im / ‖a✝‖) + π = Real.arcsin ((-a✝).im / ‖a✝‖) + π
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ ↑(rexp (Real.log ‖x‖) ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I) =
    ↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)

Tactic:
Real.exp_log

Goal state after:
case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ ↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I) =
    ↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)

case inr
x : ℂ
y : ℝ
hx : x ≠ 0
⊢ 0 < ‖x‖
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs✝ : ¬y = 0
h_ifs : ¬x = 0
⊢ rexp (log (x * y) * z) = rexp (log x * z) * y ^ z

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:
· rw [log_mul ‹_› ‹_›, add_mul, exp_add, rpow_def_of_pos (hy.lt_of_ne' ‹_›)]

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

case hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ 0 ≤ x * y
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: p : ℝ × ℝ
hp_fst : p.1 < 0
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, x.1 < 0
x : ℝ × ℝ
hx : x.1 < 0
⊢ (fun x ↦ x.1 ^ x.2) x = (fun x ↦ rexp (log x.1 * x.2) * cos (x.2 * π)) x

Tactic:
by
      dsimp only
      rw [rpow_def_of_neg hx]

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

Goal state before:
pp: x : ℝ≥0
y z : ℝ
hx₀ : x ≠ 0
hx₁ : x ≠ 1
⊢ x ^ y = x ^ z ↔ y = z

Tactic:
by
  rw [← pos_iff_ne_zero] at hx₀
  rify at *
  grind [Real.rpow_right_inj]

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

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

Tactic:
NNReal.coe_pow,

Goal state after:
x : ℝ≥0
n : ℕ
hn : n ≠ 0
⊢ ↑(x ^ (↑n)⁻¹) ^ n = ↑x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr
x : ℝ
h : x < 0
this : 1 / 2 * π = π / 2
⊢ √x = x ^ (1 / 2)

Tactic:
rw [sqrt_eq_zero_of_nonpos h.le, rpow_def_of_neg h, this, cos_pi_div_two, mul_zero]

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

Goal state before:
pp: case neg
y z : ℝ
hyz : z ≤ y
x : ℝ≥0
hx1 : x ≤ 1
h : ¬x = 0
⊢ ↑x ^ y ≤ ↑x ^ z

Tactic:
simp [← coe_rpow_of_ne_zero h,
      NNReal.rpow_le_rpow_of_exponent_ge (bot_lt_iff_ne_bot.mpr h) hx1 hyz]

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

Goal state before:
pp: p : ℝ
a b : ℝ≥0∞
hp : 0 ≤ p
⊢ 2 ^ p * max a b ^ p = 2 ^ p * max (a ^ p) (b ^ p)

Tactic:
rw [max_rpow hp]

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

Goal state before:
pp: b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ≥0
⊢ a ^ ↑(Int.negOfNat n) = (a ^ n)⁻¹

Tactic:
NNReal.rpow_intCast,

Goal state after:
b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ≥0
⊢ a ^ Int.negOfNat n = (a ^ n)⁻¹
Module: Mathlib.LinearAlgebra.Ray

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : IsStrictOrderedRing R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
x y z : RayVector R M
hxy : SameRay R ↑((equiv R M) x) ↑((equiv R M) y)
hyz : SameRay R ↑((equiv R M) y) ↑((equiv R M) z)
⊢ SameRay R ↑((equiv R M) x) ↑((equiv R M) z)

Tactic:
exact hxy.trans hyz fun hy => (y.2 hy).elim

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

Goal state before:
pp: case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Semiring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : ZeroLEOneClass 𝕜
inst✝ : Module 𝕜 E
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hb' : 0 < b
ha' : 0 < a
⊢ a • x + b • y ∈ openSegment 𝕜 x y

Tactic:
exact ⟨a, b, ha', hb', hab, rfl⟩

Goal state after:
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
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Icc 0 1
⊢ (AffineMap.lineMap x y) a✝¹ = (1 - a✝¹) • x + a✝¹ • y

Tactic:
exact AffineMap.lineMap_apply_module _ _ _

Goal state after:
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
x y : E
a✝¹ : 𝕜
a✝ : a✝¹ ∈ Ioo 0 1
⊢ (AffineMap.lineMap x y) a✝¹ = (1 - a✝¹) • x + a✝¹ • y

Tactic:
exact AffineMap.lineMap_apply_module _ _ _

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : x ≤ z
hyz : z ≤ y
⊢ z ∈ [x -[𝕜] y]

Tactic:
obtain rfl | h := (hxz.trans hyz).eq_or_lt

Goal state after:
case inl
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x z : 𝕜
hxz : x ≤ z
hyz : z ≤ x
⊢ z ∈ [x -[𝕜] x]

case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
x y z : 𝕜
hxz : x ≤ z
hyz : z ≤ y
h : x < y
⊢ z ∈ [x -[𝕜] y]
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 ∈ ⊤
hpv : (v +ᵥ p) -ᵥ p ∈ ⊤.direction
⊢ v ∈ ⊤.direction

Tactic:
rwa [vadd_vsub] at hpv

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E × F
⊢ [x -[𝕜] y] ⊆ [x.1 -[𝕜] y.1] ×ˢ [x.2 -[𝕜] y.2]

Tactic:
rintro z ⟨a, b, ha, hb, hab, hz⟩
  exact ⟨⟨a, b, ha, hb, hab, congr_arg Prod.fst hz⟩, a, b, ha, hb, hab, congr_arg Prod.snd hz⟩

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E × F
⊢ openSegment 𝕜 x y ⊆ openSegment 𝕜 x.1 y.1 ×ˢ openSegment 𝕜 x.2 y.2

Tactic:
rintro z ⟨a, b, ha, hb, hab, hz⟩
  exact ⟨⟨a, b, ha, hb, hab, congr_arg Prod.fst hz⟩, a, b, ha, hb, hab, congr_arg Prod.snd hz⟩

Goal state after:
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Bornology M
inst✝ : SMul M α
s : Set α
ι : Type u_3
t : ι → Set α
I : Set ι
hI : I.Finite
⊢ Absorbs M s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, Absorbs M s (t i)

Tactic:
simp [Absorbs, hI]

Goal state after:
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: G₀ : Type u_1
α : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : Bornology G₀
inst✝ : MulAction G₀ α
s : Set α
a : G₀
ha : a ≠ 0
⊢ s ⊆ a • univ

Tactic:
rw [smul_set_univ₀ ha]; apply subset_univ

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

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

Tactic:
simp only [Submodule.mem_iInf] at hv

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