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

Goal state before:
pp: case mk
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
g : NormedAddGroupHom V₁ V₂
toFun✝ : V₁ → V₂
map_add'✝ : ∀ (v₁ v₂ : V₁), toFun✝ (v₁ + v₂) = toFun✝ v₁ + toFun✝ v₂
bound'✝ : ∃ C, ∀ (v : V₁), ‖toFun✝ v‖ ≤ C * ‖v‖
H : ⇑{ toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ } = ⇑g
⊢ { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
toFun✝¹ : V₁ → V₂
map_add'✝¹ : ∀ (v₁ v₂ : V₁), toFun✝¹ (v₁ + v₂) = toFun✝¹ v₁ + toFun✝¹ v₂
bound'✝¹ : ∃ C, ∀ (v : V₁), ‖toFun✝¹ v‖ ≤ C * ‖v‖
toFun✝ : V₁ → V₂
map_add'✝ : ∀ (v₁ v₂ : V₁), toFun✝ (v₁ + v₂) = toFun✝ v₁ + toFun✝ v₂
bound'✝ : ∃ C, ∀ (v : V₁), ‖toFun✝ v‖ ≤ C * ‖v‖
H :
  ⇑{ toFun := toFun✝¹, map_add' := map_add'✝¹, bound' := bound'✝¹ } =
    ⇑{ toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }
⊢ { toFun := toFun✝¹, map_add' := map_add'✝¹, bound' := bound'✝¹ } =
    { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }
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₂ : V₁
⊢ ⟨φ (v₁ + v₂), ⋯⟩ = ⟨φ v₁, ⋯⟩ + ⟨φ v₂, ⋯⟩

Tactic:
ext
    simp only [map_add, AddSubgroup.coe_add]

Goal state after:
Module: Mathlib.Topology.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
E₁ : Type u_5
E₂ : Type u_6
inst✝⁷ : UniformSpace E₁
inst✝⁶ : UniformSpace E₂
inst✝⁵ : Ring E₁
inst✝⁴ : IsUniformAddGroup E₁
inst✝³ : Algebra R E₁
inst✝² : Ring E₂
inst✝¹ : IsUniformAddGroup E₂
inst✝ : Algebra R E₂
e : E₁ ≃ₐ[R] E₂
h₁ : Continuous[inst✝⁷.toTopologicalSpace, inst✝⁶.toTopologicalSpace] ⇑e
h₂ : Continuous[inst✝⁶.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑e.symm
⊢ Continuous[inst✝⁶.toTopologicalSpace, inst✝⁷.toTopologicalSpace] e.invFun

Tactic:
dsimp; fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
L : SummationFilter β
γ : Type u_5
inst✝³ : DivisionSemiring γ
inst✝² : Module γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
hg : g ≠ 0
⊢ ∑'[L] (i : β), g • f i = g • ∑'[L] (i : β), f i

Tactic:
· exact tsum_const_smul' (Units.mk0 g hg)

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝¹ : RingHomInvPair σ σ'
inst✝ : RingHomInvPair σ' σ
L : SummationFilter ι
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
h : HasSum f (e.symm y) L
⊢ HasSum (fun b ↦ e (f b)) y L

Tactic:
simpa only [e.coe_coe, e.apply_symm_apply] using (e : M →SL[σ] M₂).hasSum h

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) + (x₁ * y₂ + y₁ * x₂) • I' =
    ((algebraMap ℝ A) x₁ + y₁ • I') * ((algebraMap ℝ A) x₂ + y₂ • I')

Tactic:
add_mul,

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) + (x₁ * y₂ + y₁ * x₂) • I' =
    (algebraMap ℝ A) x₁ * ((algebraMap ℝ A) x₂ + y₂ • I') + y₁ • I' * ((algebraMap ℝ A) x₂ + y₂ • I')
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
tfae_1_to_4 : (starRingEnd K) z = z → im z = 0
tfae_4_to_3 : im z = 0 → ↑(re z) = z
tfae_3_to_2 : ↑(re z) = z → ∃ r, ↑r = z
⊢ [(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(re z) = z, im z = 0, IsSelfAdjoint z].TFAE

Tactic:
tfae_have 2 → 1 := fun ⟨r, hr⟩ => hr ▸ conj_ofReal _

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
tfae_1_to_4 : (starRingEnd K) z = z → im z = 0
tfae_4_to_3 : im z = 0 → ↑(re z) = z
tfae_3_to_2 : ↑(re z) = z → ∃ r, ↑r = z
tfae_2_to_1 : (∃ r, ↑r = z) → (starRingEnd K) z = z
⊢ [(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(re z) = z, im z = 0, IsSelfAdjoint z].TFAE
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
tfae_1_to_4 : (starRingEnd K) z = z → im z = 0
tfae_4_to_3 : im z = 0 → ↑(re z) = z
tfae_3_to_2 : ↑(re z) = z → ∃ r, ↑r = z
tfae_2_to_1 : (∃ r, ↑r = z) → (starRingEnd K) z = z
tfae_1_to_5 : (starRingEnd K) z = z → IsSelfAdjoint z
hz : IsSelfAdjoint z
⊢ (starRingEnd K) z = z

Tactic:
by rwa [isSelfAdjoint_iff] at hz

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
z : ℂ
a : A
⊢ ℑ (z • a) = z.re • ℑ a + z.im • ℜ a

Tactic:
by
  have := by congrm (ℑ ($((re_add_im z).symm) • a))
  simpa [-re_add_im, add_smul, ← smul_smul]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
⊢ ‖x + (starRingEnd K) x‖ ^ 2 = re (x + (starRingEnd K) x) ^ 2

Tactic:
rw [add_conj, ← ofReal_ofNat, ← ofReal_mul, norm_ofReal, sq_abs, ofReal_re]

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : OpenPartialHomeomorph X Y
f : Z → X
h : f ⁻¹' e.source = univ
⊢ Continuous[inst✝, inst✝²] f ↔ Continuous[inst✝, inst✝¹] (↑e ∘ f)

Tactic:
by
  simp only [← continuousOn_univ]
  exact e.continuousOn_iff_continuousOn_comp_left (Eq.symm h).subset

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ IsClosed ({a | re a.1 ≤ re a.2} ∩ {a | im a.1 = im a.2})

Tactic:
refine IsClosed.inter (isClosed_le ?_ ?_) (isClosed_eq ?_ ?_)

Goal state after:
case refine_1
K : Type u_1
inst✝ : RCLike K
⊢ Continuous fun a ↦ re a.1

case refine_2
K : Type u_1
inst✝ : RCLike K
⊢ Continuous fun a ↦ re a.2

case refine_3
K : Type u_1
inst✝ : RCLike K
⊢ Continuous fun a ↦ im a.1

case refine_4
K : Type u_1
inst✝ : RCLike K
⊢ Continuous fun a ↦ im a.2
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
h : I = 0
⊢ ∀ (x y : K), re (x * y) = re x * re y

Tactic:
simp [im_eq_zero h]

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
h : I = 0
z : K
⊢ ‖{ toFun := (realRingEquiv h).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (realRingEquiv h).invFun, left_inv := ⋯,
          right_inv := ⋯ }
        (↑(re z) + ↑(im z) * I)‖ =
    ‖↑(re z) + ↑(im z) * I‖

Tactic:
simp [-re_add_im, h]

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ ∀ (x y : ℝ), 0 ≤ x → x < y → ∃ a, x < ‖a‖ ∧ ‖a‖ < y

Tactic:
exact h.lt_norm_lt

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

Goal state before:
pp: α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
x : α
hx : c * ‖f x‖ ≤ ‖g x‖
⊢ ‖f x‖ ≤ c⁻¹ * ‖g x‖

Tactic:
rwa [← inv_inv c, inv_mul_le_iff₀ (by positivity)] at hx

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

Goal state before:
pp: case mp.zero
α : 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 : f =o[l] g
x : α
h₀' : ‖f x‖ ≤ 1 * ‖g x‖
hf : ∀ (x : α), 0 ≤ ‖f x‖
⊢ ‖f x‖ ≤ ‖g x‖

Tactic:
rwa [one_mul] at h₀'

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
c : ℝ
g' : α → F'
l : Filter α
hc : 0 ≤ c
x : α
⊢ x ∈ {x | (fun x ↦ ‖0‖ ≤ c * ‖g' x‖) x}

Tactic:
simpa using mul_nonneg hc (norm_nonneg <| g' x)

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

Goal state before:
pp: α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
h₁ : f₁ =o[l] g₁
h₂ : f₂ =O[l] g₂
⊢ (fun x ↦ f₁ x * f₂ x) =o[l] fun x ↦ g₁ x * g₂ x

Tactic:
by
  simp only [IsLittleO_def] at *
  intro c cpos
  rcases h₂.exists_pos with ⟨c', c'pos, hc'⟩
  exact ((h₁ (div_pos cpos c'pos)).mul hc').congr_const (div_mul_cancel₀ _ (ne_of_gt c'pos))

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

Goal state before:
pp: x : ℂ
n : ℕ
⊢ cexp ((↑n + 1) * x) = cexp x ^ n * cexp x

Tactic:
add_mul,

Goal state after:
x : ℂ
n : ℕ
⊢ cexp (↑n * x + 1 * x) = cexp x ^ n * cexp x
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case mpr
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ (∃ φ, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v) → u =O[l] v

Tactic:
rintro ⟨φ, ⟨c, hφ⟩, huvφ⟩
    exact isBigO_iff_isBigOWith.2 ⟨c, isBigOWith_of_eq_mul φ hφ huvφ⟩

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

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

Tactic:
add_mul,

Goal state after:
x y : ℂ
⊢ sinh (x * I + y * I) = (sin x * cos y + cos x * sin y) * I
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
add_mul,

Goal state after:
x y : ℂ
⊢ sinh (x * I + y * I) = sin x * cos y * I + cos x * sin y * I
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
add_mul,

Goal state after:
x y : ℂ
⊢ cosh (x * I + y * I) = cos x * cos y - sin x * sin y
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ sin x * cos x + cos x * sin x = (sin x + sin x) * cos x

Tactic:
add_mul,

Goal state after:
x : ℂ
⊢ sin x * cos x + cos x * sin x = sin x * cos x + sin x * cos x
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
simp [sinh_three_mul]

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

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + x ^ 2) * (1 - x)
⊢ ∑ m ∈ range 3, x ^ m / ↑m.factorial + x ^ 3 * (↑3 + 1) / (↑(Nat.factorial 3) * ↑3) ≤ 1 + x + x ^ 2

Tactic:
rw [show 3 = 1 + 1 + 1 from rfl]

Goal state after:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + x ^ 2) * (1 - x)
⊢ ∑ m ∈ range (1 + 1 + 1), x ^ m / ↑m.factorial +
      x ^ (1 + 1 + 1) * (↑(1 + 1 + 1) + 1) / (↑(1 + 1 + 1).factorial * ↑(1 + 1 + 1)) ≤
    1 + x + x ^ 2
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
i : ℕ
hi : ¬(i ≥ m → a - (Nat.find h).pred • ε < f i)
⊢ ∃ i, ∀ j ≥ i, |f j - f i| < ε

Tactic:
Classical.not_imp,

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
i : ℕ
hi : i ≥ m ∧ ¬a - (Nat.find h).pred • ε < f i
⊢ ∃ i, ∀ j ≥ i, |f j - f i| < ε
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) (cexp 0) < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
⊢ dist x y < δ → dist (cexp x) (cexp y) < ε

Tactic:
hxy

Goal state after:
a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) (cexp 0) < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
hxy : dist x y < δ
⊢ dist (cexp x) (cexp y) < ε
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) (cexp 0) < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
hxy : dist x y < δ
⊢ dist (cexp x) (cexp y) < ε

Tactic:
have h3 := hδ.2 (y := x - y) (by simpa only [dist_eq_norm, sub_zero] using hxy)

Goal state after:
a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) (cexp 0) < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
hxy : dist x y < δ
h3 : dist (cexp (x - y)) (cexp 0) < ε / (2 * Real.exp a)
⊢ dist (cexp x) (cexp y) < ε
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
⊢ √(sin (x / 2) ^ 2) = √((1 - cos x) / 2)

Tactic:
sin_sq_eq_half_sub,

Goal state after:
x : ℝ
⊢ √(1 / 2 - cos (2 * (x / 2)) / 2) = √((1 - cos x) / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
h : cos x = 1
n : ℤ
hn : (1 + ↑(2 * (n / 2))) * π = x
hn1 : n % 2 = 1
⊢ ↑(n / 2) * (2 * π) = x

Tactic:
add_mul,

Goal state after:
x : ℝ
h : cos x = 1
n : ℤ
hn : 1 * π + ↑(2 * (n / 2)) * π = x
hn1 : n % 2 = 1
⊢ ↑(n / 2) * (2 * π) = x
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✝ : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < ‖(mk I) a‖ + ε₁
b : R
hb : ‖b‖ < ‖(mk I) b‖ + ε₂
h : ‖a‖ * ‖b‖ - ‖(mk I) a‖ * ‖(mk I) b‖ < ε ∧ ‖(mk I) a‖ * ‖(mk I) b‖ - ‖a‖ * ‖b‖ < ε
⊢ ‖(mk I) a * (mk I) b‖ ≤ ‖(mk I) a‖ * ‖(mk I) b‖ + ε

Tactic:
calc
      _ ≤ ‖a‖ * ‖b‖ := (Ideal.Quotient.norm_mk_le I (a * b)).trans (norm_mul_le a b)
      _ ≤ _ := (sub_lt_iff_lt_add'.mp h.1).le

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]))
    simp at h1

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
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ c⁻¹ • y ∈ ball x r ↔ y ∈ ball (c • x) (‖c‖ * r)

Tactic:
conv_lhs => rw [← inv_smul_smul₀ hc x]

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
⊢ c⁻¹ • y ∈ ball (c⁻¹ • c • 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 : ℝ
y : E
⊢ c⁻¹ • y ∈ sphere x r ↔ y ∈ sphere (c • x) (‖c‖ * r)

Tactic:
conv_lhs => rw [← inv_smul_smul₀ hc x]

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
⊢ c⁻¹ • y ∈ sphere (c⁻¹ • c • x) r ↔ y ∈ sphere (c • x) (‖c‖ * r)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 6) = 1 / 2

Tactic:
rw [← cos_pi_div_two_sub, ← cos_pi_div_three]
  congr
  ring

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

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ (1 + x) * ∑' (i : ℕ), x ^ i = 2 * ∑' (i : ℕ), x ^ i - 1

Tactic:
add_mul,

Goal state after:
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ 1 * ∑' (i : ℕ), x ^ i + x * ∑' (i : ℕ), x ^ i = 2 * ∑' (i : ℕ), x ^ i - 1
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 i ↦ x ^ i) (1 - x)⁻¹ʳ

Tactic:
by
  convert! (summable_geometric_of_norm_lt_one h).hasSum
  exact (geom_series_eq_inverse x h).symm

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

Goal state before:
pp: case succ
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n ↦ ↑((n + k).choose k) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
I1 : Summable fun n ↦ ‖↑((n + k).choose k) * r ^ n‖
⊢ HasSum (fun n ↦ ↑((n + (k + 1)).choose (k + 1)) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1 + 1))

Tactic:
convert!
        hasSum_sum_range_mul_of_summable_norm' I1 ih.summable
          (summable_norm_geometric_of_norm_lt_one hr) (summable_geometric_of_norm_lt_one hr) with
        n

Goal state after:
case e'_5
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n ↦ ↑((n + k).choose k) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
I1 : Summable fun n ↦ ‖↑((n + k).choose k) * r ^ n‖
n : ℕ
⊢ ↑((n + (k + 1)).choose (k + 1)) * r ^ n =
    ∑ k_1 ∈ Finset.range (n + 1), ↑((k_1 + k).choose k) * r ^ k_1 * r ^ (n - k_1)

case e'_6
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
r : R
hr : ‖r‖ < 1
k : ℕ
ih : HasSum (fun n ↦ ↑((n + k).choose k) * r ^ n) ((1 - r)⁻¹ʳ ^ (k + 1))
I1 : Summable fun n ↦ ‖↑((n + k).choose k) * r ^ n‖
⊢ (1 - r)⁻¹ʳ ^ (k + 1 + 1) = (∑' (n : ℕ), ↑((n + k).choose k) * r ^ n) * ∑' (n : ℕ), r ^ n
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace T
K : Set X
U✝ : Set Y
inst✝ : LocallyCompactPair X Y
f : C(X, Y)
x : X
U : Set Y
hx : f x ∈ U
hU : IsOpen[inst✝³] U
⊢ ∀ᶠ (x : C(X, Y) × X) in 𝓝 (f, x), x.1 x.2 ∈ U

Tactic:
rcases exists_mem_nhds_isCompact_mapsTo f.continuous (hU.mem_nhds hx) with ⟨K, hxK, hK, hKU⟩

Goal state after:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace T
K✝ : Set X
U✝ : Set Y
inst✝ : LocallyCompactPair X Y
f : C(X, Y)
x : X
U : Set Y
hx : f x ∈ U
hU : IsOpen[inst✝³] U
K : Set X
hxK : K ∈ 𝓝 x
hK : IsCompact K
hKU : MapsTo (⇑f) K U
⊢ ∀ᶠ (x : C(X, Y) × X) in 𝓝 (f, x), x.1 x.2 ∈ U
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
⊢ IsPathConnected (range f)

Tactic:
rw [← image_univ]
  exact isPathConnected_univ.image hf

Goal state after:
Module: Mathlib.Topology.Instances.ZMultiples

Goal state before:
pp: ⊢ Tendsto Int.cast Filter.cofinite (cocompact ℝ)

Tactic:
by
  apply (castAddHom ℝ).tendsto_coe_cofinite_of_discrete cast_injective
  rw [range_castAddHom, SetLike.isDiscrete_iff_discreteTopology]
  infer_instance

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Real

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
x y : ZMod N
⊢ toAddCircle x = toAddCircle y → x = y

Tactic:
hxy

Goal state after:
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : toAddCircle x = toAddCircle y
⊢ x = y
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: x : ℝ
⊢ ‖↑x‖ = |x|

Tactic:
suffices { y : ℝ | (y : AddCircle (0 : ℝ)) = (x : AddCircle (0 : ℝ)) } = {x} by
    simp [norm_eq_infDist, this]

Goal state after:
x : ℝ
⊢ {y | ↑y = ↑x} = {x}
Module: Mathlib.Topology.Path

Goal state before:
pp: case refine_2
X : Type u_1
inst✝¹ : TopologicalSpace X
ι : Type u_4
inst✝ : TopologicalSpace ι
a b c : ι → X
γ₁ : (t : ι) → Path (a t) (b t)
h₁ : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ₁
γ₂ : (t : ι) → Path (b t) (c t)
h₂ : Continuous[instTopologicalSpaceProd, inst✝¹] ↿γ₂
h₁' : Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ₁ t).extend
h₂' : Continuous[instTopologicalSpaceProd, inst✝¹] ↿fun t ↦ ⇑(γ₂ t).extend
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] ((fun p ↦ (γ₂ p.1).extend p.2) ∘ Prod.map id fun x ↦ 2 * ↑x - 1)

Tactic:
exact h₂'.comp (by fun_prop)

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

Goal state before:
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 [inv_mul_lt_iff₀ hp, ← mul_div_assoc, mul_one]

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

Goal state before:
pp: case inl
E : Type u_5
inst✝⁶ : Ring E
inst✝⁵ : LinearOrder E
inst✝⁴ : IsOrderedRing E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : CompleteSpace E
inst✝ : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
h✝ : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 (∑' (i : ℕ), (-1) ^ i * f i))
lower : ∀ (k : ℕ), ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * k + 1), (-1) ^ i * f i
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
upper : ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ ∑' (i : ℕ), (-1) ^ i * f i
h : Even (2 * n)
⊢ |∑' (i : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i| ≤ f (2 * n)

Tactic:
specialize lower n

Goal state after:
case inl
E : Type u_5
inst✝⁶ : Ring E
inst✝⁵ : LinearOrder E
inst✝⁴ : IsOrderedRing E
inst✝³ : UniformSpace E
inst✝² : IsUniformAddGroup E
inst✝¹ : CompleteSpace E
inst✝ : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
h✝ : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 (∑' (i : ℕ), (-1) ^ i * f i))
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
lower : ∑' (i : ℕ), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n + 1), (-1) ^ i * f i
upper : ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ ∑' (i : ℕ), (-1) ^ i * f i
h : Even (2 * n)
⊢ |∑' (i : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i| ≤ f (2 * n)