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
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
hQ0 : Q ≠ 0
h2Q0 : 2 * Q ≠ 0
hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε
hNMK : max N M + 1 < K
hKN : N < K
hsumlesum :
  ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) ≤
    ∑ i ∈ range (max N M + 1), abv (f i) * (ε / (2 * P))
hsumltP : ∑ n ∈ range (max N M + 1), abv (f n) < P
⊢ ε / (2 * P) * ∑ i ∈ range (max N M + 1), abv (f i) < ε / (2 * P) * P

Tactic:
;

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
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
hQ0 : Q ≠ 0
h2Q0 : 2 * Q ≠ 0
hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε
hNMK : max N M + 1 < K
hKN : N < K
hsumlesum :
  ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) ≤
    ∑ i ∈ range (max N M + 1), abv (f i) * (ε / (2 * P))
hsumltP : ∑ n ∈ range (max N M + 1), abv (f n) < P
⊢ ε / (2 * P) * ∑ i ∈ range (max N M + 1), abv (f i) < ε / (2 * P) * P
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑(cosh (3 * x)) = ↑(4 * cosh x ^ 3 - 3 * cosh x)

Tactic:
;

Goal state after:
x : ℝ
⊢ ↑(cosh (3 * x)) = ↑(4 * cosh x ^ 3 - 3 * cosh x)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑(sinh (3 * x)) = ↑(4 * sinh x ^ 3 + 3 * sinh x)

Tactic:
;

Goal state after:
x : ℝ
⊢ ↑(sinh (3 * x)) = ↑(4 * sinh x ^ 3 + 3 * sinh x)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ↑‖1‖₊ = 1

Tactic:
;

Goal state after:
x : ℝ
⊢ ↑‖1‖₊ = 1
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖cexp (-(↑x / 2 * I)) * (cexp ((↑x / 2 + -(↑x / 2)) * I) - cexp ((↑x / 2 + ↑x / 2) * I)) * I‖

Tactic:
;

Goal state after:
x : ℝ
⊢ ‖cexp (I * ↑x) - 1‖ = ‖cexp (-(↑x / 2 * I)) * (cexp ((↑x / 2 + -(↑x / 2)) * I) - cexp ((↑x / 2 + ↑x / 2) * I)) * I‖
Module: Mathlib.Analysis.Complex.Exponential

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

Tactic:
;

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.Complex.Trigonometric

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

Tactic:
;

Goal state after:
x : ℝ
⊢ -(x / 2) = -x / 2
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
k : ℤ
⊢ 0 ≤ a ^ (k + k)

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
k : ℤ
⊢ 0 ≤ a ^ (k + k)
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
k : ℤ
⊢ 0 ≤ a ^ k * a ^ k

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
k : ℤ
⊢ 0 ≤ a ^ k * a ^ k
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
n : ℤ
hn : Odd n
⊢ a < 0 ∨ a ^ n = 0 ↔ a < 0 ∨ a = 0

Tactic:
zpow_eq_zero_iff

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
n : ℤ
hn : Odd n
⊢ a < 0 ∨ a = 0 ↔ a < 0 ∨ a = 0

α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
n : ℤ
hn : Odd n
⊢ n ≠ 0
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : |rexp 1 - expNear m 1 ((a₁ - 1) * ↑m)| ≤ |1| ^ m / ↑m.factorial * (b₁ * ↑m)
⊢ ¬m = 0

Tactic:
;

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

Goal state before:
pp: R : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : NormedRing R
f : ι → R
g : ι' → R
hf : Summable fun x ↦ ‖f x‖
h'f : Summable f
hg : Summable fun x ↦ ‖g x‖
h'g : Summable g
⊢ Summable fun x ↦ f x.1 * g x.2

Tactic:
classical
  suffices HasSum (fun x : ι × ι' => f x.1 * g x.2) ((∑' i, f i) * (∑' j, g j)) from this.summable
  let s : Finset ι × Finset ι' → Finset (ι × ι') := fun p ↦ p.1 ×ˢ p.2
  apply hasSum_of_subseq_of_summable (hf.mul_norm hg) tendsto_finsetProd_atTop
  rw [← prod_atTop_atTop_eq]
  have := Tendsto.prodMap h'f.hasSum h'g.hasSum
  rw [← nhds_prod_eq] at this
  convert!
    ((continuous_mul (M := R)).continuousAt (x := (∑' (i : ι), f i, ∑' (j : ι'), g j))).tendsto.comp
      this with
    p
  simp [sum_product, ← mul_sum, ← sum_mul]

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: case h
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
hg : Summable fun x ↦ ‖g x‖
this : Summable fun n ↦ ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖
n : ℕ
kl : ℕ × ℕ
a✝ : kl ∈ antidiagonal n
⊢ ‖f kl.1 * g kl.2‖ ≤ ‖f kl.1‖ * ‖g kl.2‖

Tactic:
;

Goal state after:
case h
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
hg : Summable fun x ↦ ‖g x‖
this : Summable fun n ↦ ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖
n : ℕ
kl : ℕ × ℕ
a✝ : kl ∈ antidiagonal n
⊢ ‖f kl.1 * g kl.2‖ ≤ ‖f kl.1‖ * ‖g kl.2‖
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

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

Tactic:
← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l

Goal state after:
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
hg : Summable fun x ↦ ‖g x‖
⊢ Summable fun n ↦ ‖∑ ij ∈ antidiagonal n, f ij.1 * g ij.2‖
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

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

Tactic:
← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l

Goal state after:
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
h'f : Summable f
hg : Summable fun x ↦ ‖g x‖
h'g : Summable g
⊢ Summable fun n ↦ ∑ ij ∈ antidiagonal n, f ij.1 * g ij.2
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‖
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ range (n + 1), f k * g (n - k)

Tactic:
← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l

Goal state after:
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 = ∑' (n : ℕ), ∑ ij ∈ antidiagonal n, f ij.1 * g ij.2
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

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

Tactic:
← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l

Goal state after:
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x ↦ ‖f x‖
h'f : Summable f
hg : Summable fun x ↦ ‖g x‖
h'g : Summable g
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ ij ∈ antidiagonal n, f ij.1 * g ij.2
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ (1 - t / ↑n) ^ n ≤ rexp (-(t / ↑n)) ^ n

Tactic:
by
      gcongr
      · exact sub_nonneg.2 <| div_le_one_of_le₀ ht' n.cast_nonneg
      · exact one_sub_le_exp_neg _

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

Goal state before:
pp: case h
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ ↑n ≠ 0

Tactic:
;

Goal state after:
case h
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ ↑n ≠ 0
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
hrec : ∀ᶠ (n₀ : ℕ) in atTop, ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
⊢ ∀ (a : ℕ), 0 ≤ f a → 0 < g a → g a = 0 → f a = 0

Tactic:
;

Goal state after:
f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
hrec : ∀ᶠ (n₀ : ℕ) in atTop, ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
⊢ ∀ (a : ℕ), 0 ≤ f a → 0 < g a → g a = 0 → f a = 0
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 • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l = 0
this : f m > a - l • ε
⊢ a < f m

Tactic:
;

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 • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l = 0
this : f m > a - l • ε
⊢ a < f m
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case bc
α : 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 • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := ⋯
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find h).pred • ε
j : ℕ
hj : j ≥ i
hfij : f j ≤ f i
⊢ a - l • ε < f j

Tactic:
;

Goal state after:
case bc
α : 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 • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := ⋯
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l ≠ 0
i : ℕ
hi : i ≥ m ∧ f i ≤ a - (Nat.find h).pred • ε
j : ℕ
hj : j ≥ i
hfij : f j ≤ f i
⊢ a - l • ε < f j
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: ⊢ Continuous fun x ↦ (Complex.exp ↑x).re

Tactic:
;

Goal state after:
⊢ Continuous fun x ↦ (Complex.exp ↑x).re
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: case hab
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ x ≤ ↑⌈x⌉₊

Tactic:
;

Goal state after:
case hab
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ x ≤ ↑⌈x⌉₊
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: case a
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ ↑⌈x⌉₊ ≤ x + 1

Tactic:
;

Goal state after:
case a
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ ↑⌈x⌉₊ ≤ x + 1
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
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) →
      ∀ (m : ℕ), n.succ ≤ m → m = k + n.succ → abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
⊢ k + (0 + n.succ) ≥ 0 + n.succ

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) →
      ∀ (m : ℕ), n.succ ≤ m → m = k + n.succ → abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
⊢ k + (0 + n.succ) ≥ 0 + n.succ
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:
;

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

Goal state before:
pp: ⊢ 1 ≤ π / 2

Tactic:
;

Goal state after:
⊢ 1 ≤ π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 2) * 0 + 0 * sin (π / 2) = 0

Tactic:
;

Goal state after:
⊢ sin (π / 2) * 0 + 0 * sin (π / 2) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
⊢ sin x = 0 ↔ ∃ n, ↑n * π = x

Tactic:
;

Goal state after:
x : ℝ
⊢ sin x = 0 ↔ ∃ n, ↑n * π = x
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedGroup E
s : Set E
⊢ IsBounded s → IsBounded s⁻¹

Tactic:
by
  simp_rw [isBounded_iff_forall_norm_le', ← image_inv_eq_inv, forall_mem_image, norm_inv']
  exact id

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
__spread✝⁻⁰ : M ⧸ S ≃ M ⧸ S := Subgroup.quotientEquivOfEq ⋯
⊢ Isometry (Subgroup.quotientEquivOfEq ⋯).toFun

Tactic:
;

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
__spread✝⁻⁰ : M ⧸ S ≃ M ⧸ S := Subgroup.quotientEquivOfEq ⋯
⊢ Isometry (Subgroup.quotientEquivOfEq ⋯).toFun
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: case mk.mk
M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
__spread✝⁻⁰ : M ⧸ S ≃ M ⧸ S := Subgroup.quotientEquivOfEq ⋯
x1✝ : M ⧸ S
a✝¹ : M
x2✝ : M ⧸ S
a✝ : M
⊢ edist ((Subgroup.quotientEquivOfEq ⋯).toFun (Quot.mk (⇑(leftRel S)) a✝¹))
      ((Subgroup.quotientEquivOfEq ⋯).toFun (Quot.mk (⇑(leftRel S)) a✝)) =
    edist (Quot.mk (⇑(leftRel S)) a✝¹) (Quot.mk (⇑(leftRel S)) a✝)

Tactic:
;

Goal state after:
case mk.mk
M : Type u_1
inst✝ : SeminormedCommGroup M
S : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
__spread✝⁻⁰ : M ⧸ S ≃ M ⧸ S := Subgroup.quotientEquivOfEq ⋯
x1✝ : M ⧸ S
a✝¹ : M
x2✝ : M ⧸ S
a✝ : M
⊢ edist ((Subgroup.quotientEquivOfEq ⋯).toFun (Quot.mk (⇑(leftRel S)) a✝¹))
      ((Subgroup.quotientEquivOfEq ⋯).toFun (Quot.mk (⇑(leftRel S)) a✝)) =
    edist (Quot.mk (⇑(leftRel S)) a✝¹) (Quot.mk (⇑(leftRel S)) a✝)
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
r : ℝ
z : M
h₁ : ∀ (m : M), ↑m = (quotientQuotientEquivQuotient S T h) ↑↑z → r ≤ ‖m‖
⊢ ↑z = (quotientQuotientEquivQuotient S T h) ↑↑z

Tactic:
;

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.Group.Quotient

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : SeminormedAddCommGroup M
inst✝² : SeminormedAddCommGroup N
R : Type u_3
inst✝¹ : Ring R
inst✝ : Module R M
S : Submodule R M
__spread✝⁻⁰ : (M ⧸ S) ≃ₗ[R] M ⧸ S := S.quotEquivOfEq S ⋯
⊢ ∀ (x : M ⧸ S), ‖(S.quotEquivOfEq S ⋯) x‖ = ‖x‖

Tactic:
;

Goal state after:
M : Type u_1
N : Type u_2
inst✝³ : SeminormedAddCommGroup M
inst✝² : SeminormedAddCommGroup N
R : Type u_3
inst✝¹ : Ring R
inst✝ : Module R M
S : Submodule R M
__spread✝⁻⁰ : (M ⧸ S) ≃ₗ[R] M ⧸ S := S.quotEquivOfEq S ⋯
⊢ ∀ (x : M ⧸ S), ‖(S.quotEquivOfEq S ⋯) x‖ = ‖x‖
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: case mk
M : Type u_1
N : Type u_2
inst✝³ : SeminormedAddCommGroup M
inst✝² : SeminormedAddCommGroup N
R : Type u_3
inst✝¹ : Ring R
inst✝ : Module R M
S : Submodule R M
__spread✝⁻⁰ : (M ⧸ S) ≃ₗ[R] M ⧸ S := S.quotEquivOfEq S ⋯
x✝ : M ⧸ S
a✝ : M
⊢ ‖(S.quotEquivOfEq S ⋯) (Quot.mk (⇑S.quotientRel) a✝)‖ = ‖Quot.mk (⇑S.quotientRel) a✝‖

Tactic:
;

Goal state after:
case mk
M : Type u_1
N : Type u_2
inst✝³ : SeminormedAddCommGroup M
inst✝² : SeminormedAddCommGroup N
R : Type u_3
inst✝¹ : Ring R
inst✝ : Module R M
S : Submodule R M
__spread✝⁻⁰ : (M ⧸ S) ≃ₗ[R] M ⧸ S := S.quotEquivOfEq S ⋯
x✝ : M ⧸ S
a✝ : M
⊢ ‖(S.quotEquivOfEq S ⋯) (Quot.mk (⇑S.quotientRel) a✝)‖ = ‖Quot.mk (⇑S.quotientRel) a✝‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x y : ℝ
h : x ≤ y
n : ℕ
⊢ √(2 + x.sqrtTwoAddSeries n) ≤ √(2 + y.sqrtTwoAddSeries n)

Tactic:
;

Goal state after:
x y : ℝ
h : x ≤ y
n : ℕ
⊢ √(2 + x.sqrtTwoAddSeries n) ≤ √(2 + y.sqrtTwoAddSeries n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case h₂
x y : ℝ
h : x ≤ y
n : ℕ
⊢ x.sqrtTwoAddSeries n ≤ y.sqrtTwoAddSeries n

Tactic:
;

Goal state after:
case h₂
x y : ℝ
h : x ≤ y
n : ℕ
⊢ x.sqrtTwoAddSeries n ≤ y.sqrtTwoAddSeries n
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case h
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ 0 ≤ r

Tactic:
;

Goal state after:
case h
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
x y : E
h : r ∈ Icc 0 1
⊢ 0 ≤ r
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case e'_5
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt (fun c ↦ c • (y - x) + x) (Ico 0 1) 1
⊢ y = 1 • (y - x) + x

Tactic:
rw [one_smul, sub_add_cancel]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

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

Tactic:
have h1 : (1 : ℝ) ∈ interior (Icc (-1 : ℝ) 1) :=
      interior_mono this (preimage_interior_subset_interior_preimage (by fun_prop) (by simpa [f]))

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c ↦ c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
h1 : 1 ∈ interior (Icc (-1) 1)
⊢ y ∈ ball x (dist y x)
Module: Mathlib.Topology.Hom.ContinuousEvalConst

Goal state before:
pp: F : Type u_1
α : Type u_2
X : Type u_3
inst✝⁵ : FunLike F α X
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalSpace X
inst✝² : ContinuousEvalConst F α X
F' : Type u_5
inst✝¹ : FunLike F' α X
inst✝ : TopologicalSpace F'
f : F' → F
hc : Continuous[inst✝, inst✝⁴] f
hf : ∀ (g : F'), ⇑(f g) = ⇑g
x : α
⊢ Continuous[inst✝, inst✝³] fun f ↦ f x

Tactic:
by simpa only [← hf] using! (continuous_eval_const x).comp hc

Goal state after:
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
s : Set 𝕜
hs : 0 ∉ s
r : ℝ
x✝ : E
⊢ x✝ ∈ ⋃ c ∈ s, sphere 0 (‖c‖ * r) ↔ x✝ ∈ (fun x ↦ ‖x‖) ⁻¹' (fun x ↦ ‖x‖ * r) '' s

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set 𝕜
hs : 0 ∉ s
r : ℝ
x✝ : E
⊢ x✝ ∈ ⋃ c ∈ s, sphere 0 (‖c‖ * r) ↔ x✝ ∈ (fun x ↦ ‖x‖) ⁻¹' (fun x ↦ ‖x‖ * r) '' s
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case h₁
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
hr : r ∈ closedBall 0 (ε / R)
y : E
hy : y ∈ (fun x_1 ↦ -x + x_1) ⁻¹' (r • s)
z : E
zs : z ∈ s
hz : r • z = -x + y
⊢ ‖r‖ ≤ ε / R

pp: case h₂
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : closedBall 0 (ε / R) ∈ 𝓝 0
r : 𝕜
hr : r ∈ closedBall 0 (ε / R)
y : E
hy : y ∈ (fun x_1 ↦ -x + x_1) ⁻¹' (r • s)
z : E
zs : z ∈ s
hz : r • z = -x + y
⊢ ‖z‖ ≤ R

Tactic:
exacts [mem_closedBall_zero_iff.1 hr, mem_closedBall_zero_iff.1 (hR zs)]

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

Goal state before:
pp: θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
n : ℤ
hn : ↑n * 5 = 1
⊢ n * 5 = 1

Tactic:
;

Goal state after:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
n : ℤ
hn : ↑n * 5 = 1
⊢ n * 5 = 1