mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : 0 < a
⊢ b * b - 4 * a * c ≤ 0

Tactic:
have ha' : 0 ≤ 4 * a := mul_nonneg zero_le_four ha.le
    convert neg_nonpos.2 (mul_nonneg ha' (h (-b / (2 * a))))
    field

Goal state after:
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝⁴ : PseudoEMetricSpace β
μ : Measure α
inst✝³ : SemilatticeSup ι
inst✝² : Nonempty ι
inst✝¹ : Countable ι
f : ι → α → β
g : α → β
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
⊢ ∃ t, MeasurableSet t ∧ μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop tᶜ

Tactic:
have ⟨t, _, ht, htendsto⟩ :=
    tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist hf MeasurableSet.univ
    (measure_ne_top μ Set.univ) (by filter_upwards [hfg] with _ htendsto _ using htendsto) hε
  refine ⟨_, ht, ?_⟩
  rwa [Set.compl_eq_univ_sdiff]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
this : (f * fun x ↦ (f x)⁻¹) ≤ᵐ[μ] 1
⊢ μ.withDensity (f * fun i ↦ (f i)⁻¹) ≤ μ

Tactic:
refine (withDensity_mono this).trans ?_
    rw [withDensity_one]

Goal state after:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: z w : ℝ
⊢ z = w → ↑z = ↑w

Tactic:
apply congrArg

Goal state after:
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
⊢ SFinite μ

Tactic:
rw [← Measure.restrict_add_restrict_compl (μ := μ) measurableSet_sigmaFiniteSetWRT,
    restrict_compl_sigmaFiniteSetWRT hμν]
  infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (x : α), ∫⁻ (y : β), φ (x, y) ∂ν ∂μ.withDensity f = ∫⁻ (a : α × β), φ a ∂(μ.prod ν).withDensity fun z ↦ f z.1

Tactic:
lintegral_withDensity_eq_lintegral_mul₀ hf,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (a : α), (f * fun x ↦ ∫⁻ (y : β), φ (x, y) ∂ν) a ∂μ = ∫⁻ (a : α × β), φ a ∂(μ.prod ν).withDensity fun z ↦ f z.1

α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun x ↦ ∫⁻ (y : β), φ (x, y) ∂ν) μ
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: E : Type u_2
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CStarRing E
inst✝ : Nontrivial E
U : ↥(unitary E)
⊢ ‖(↑U)⋆ * ↑U‖ = 1

Tactic:
Unitary.coe_star_mul_self,

Goal state after:
E : Type u_2
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CStarRing E
inst✝ : Nontrivial E
U : ↥(unitary E)
⊢ ‖1‖ = 1
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: case succ
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ ‖x ^ (2 * 2 ^ k)‖₊ = ‖x‖₊ ^ (2 * 2 ^ k)

Tactic:
pow_mul',

Goal state after:
case succ
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ ‖(x ^ 2 ^ k) ^ 2‖₊ = ‖x‖₊ ^ (2 * 2 ^ k)
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: i j : Fin 2
⊢ (basisOneI.repr (![1, I] i)) j = (Finsupp.single i 1) j

Tactic:
fin_cases i <;> fin_cases j

Goal state after:
case «0».«0»
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩))) ((fun i ↦ i) ⟨0, ⋯⟩) =
    (Finsupp.single ((fun i ↦ i) ⟨0, ⋯⟩) 1) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩))) ((fun i ↦ i) ⟨1, ⋯⟩) =
    (Finsupp.single ((fun i ↦ i) ⟨0, ⋯⟩) 1) ((fun i ↦ i) ⟨1, ⋯⟩)

case «1».«0»
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩))) ((fun i ↦ i) ⟨0, ⋯⟩) =
    (Finsupp.single ((fun i ↦ i) ⟨1, ⋯⟩) 1) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩))) ((fun i ↦ i) ⟨1, ⋯⟩) =
    (Finsupp.single ((fun i ↦ i) ⟨1, ⋯⟩) 1) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: i j : Fin 2
⊢ (LinearMap.toMatrix basisOneI basisOneI) (↑↑conjAe) i j = !![1, 0; 0, -1] i j

Tactic:
fin_cases i <;> fin_cases j

Goal state after:
case «0».«0»
⊢ (LinearMap.toMatrix basisOneI basisOneI) (↑↑conjAe) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![1, 0; 0, -1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «0».«1»
⊢ (LinearMap.toMatrix basisOneI basisOneI) (↑↑conjAe) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![1, 0; 0, -1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case «1».«0»
⊢ (LinearMap.toMatrix basisOneI basisOneI) (↑↑conjAe) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![1, 0; 0, -1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1».«1»
⊢ (LinearMap.toMatrix basisOneI basisOneI) (↑↑conjAe) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![1, 0; 0, -1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: f : ℂ →ₐ[ℝ] ℂ
⊢ f = AlgHom.id ℝ ℂ ∨ f = ↑conjAe

Tactic:
refine
      (eq_or_eq_neg_of_sq_eq_sq (f I) I <| by rw [← map_pow, I_sq, map_neg, map_one]).imp ?_ ?_ <;>
    refine fun h => algHom_ext ?_

Goal state after:
case refine_1
f : ℂ →ₐ[ℝ] ℂ
h : f I = I
⊢ f I = (AlgHom.id ℝ ℂ) I

case refine_2
f : ℂ →ₐ[ℝ] ℂ
h : f I = -I
⊢ f I = ↑conjAe I
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
a : A
⊢ ↑(ℜ a) + I • ↑(ℑ a) = a

Tactic:
simp [realPart, imaginaryPart, smul_smul, ← smul_add, inv_smul_eq_iff₀, two_smul]

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

Goal state before:
pp: z : ℂ
hz : z ≠ 0
⊢ (0 < z.re ∨ z.im ≠ 0) ∨ 0 < (-z).re ∨ (-z).im ≠ 0

Tactic:
ne_eq,

Goal state after:
z : ℂ
hz : ¬z = 0
⊢ (0 < z.re ∨ z.im ≠ 0) ∨ 0 < (-z).re ∨ (-z).im ≠ 0
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
⊢ s ⊆ slitPlane ↔ -↑r ∉ s

Tactic:
simp_rw [Set.subset_def, mem_slitPlane_iff_not_le_zero]

Goal state after:
r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
⊢ (∀ x ∈ s, ¬x ≤ 0) ↔ -↑r ∉ s
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
x y : A
h₁ : ℜ x = ℜ y
h₂ : ℑ x = ℑ y
⊢ x = y

Tactic:
by
  rw [← realPart_add_I_smul_imaginaryPart x, ← realPart_add_I_smul_imaginaryPart y, h₁, h₂]

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

Goal state before:
pp: A✝ : Type u_1
F : Type u_2
E : Type u_3
A : Type u_4
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : PartialOrder E
inst✝¹² : StarAddMonoid E
inst✝¹¹ : SelfAdjointDecompose E
inst✝¹⁰ : Module ℂ E
inst✝⁹ : StarModule ℂ E
inst✝⁸ : NonUnitalRing A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module ℂ A
inst✝³ : StarModule ℂ A
inst✝² : FunLike F E A
inst✝¹ : OrderHomClass F E A
inst✝ : LinearMapClass F ℂ E A
φ : F
x : E
⊢ φ (star (↑(ℜ x) + I • ↑(ℑ x))) = star (φ (↑(ℜ x) + I • ↑(ℑ x)))

Tactic:
simp [(ℜ x).2.map' φ, IsSelfAdjoint.star_eq, (ℑ x).2.map' φ]

Goal state after:
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
⊢ Continuous[instTopologicalSpaceSubtype, inst✝³] (f.source.domRestrict ↑f)

Tactic:
← continuous_codRestrict_iff (s := f.target) (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.source.domRestrict ↑f) f.target ⋯)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case mp
K : Type u_1
inst✝ : RCLike K
z w : K
⊢ (re z ≤ re w ∧ im z = im w) ∧ z ≠ w → (re z ≤ re w ∧ re z ≠ re w) ∧ im z = im w

Tactic:
rintro ⟨⟨hr, hi⟩, heq⟩

Goal state after:
case mp
K : Type u_1
inst✝ : RCLike K
z w : K
heq : z ≠ w
hr : re z ≤ re w
hi : im z = im w
⊢ (re z ≤ re w ∧ re z ≠ re w) ∧ im z = im w
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
s : Set Y
⊢ 𝓝[e.target ∩ s] ↑e x = 𝓝[s] ↑e x

Tactic:
e.nhdsWithin_target_inter (e.map_source hx)

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
s : Set Y
⊢ 𝓝[s] ↑e x = 𝓝[s] ↑e x
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
hz : 0 < z
⊢ 0 < z⁻¹

Tactic:
pos_iff_exists_ofReal

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
hz : ∃ x > 0, ↑x = z
⊢ 0 < z⁻¹
Module: Mathlib.Analysis.Complex.Asymptotics

Goal state before:
pp: ⊢ Int.cast =Θ[cofinite] Int.cast

Tactic:
apply Asymptotics.IsTheta.of_norm_eventuallyEq_norm

Goal state after:
⊢ (fun x ↦ ‖↑x‖) =ᶠ[cofinite] fun x ↦ ‖↑x‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =O[l] g → (f ∘ Prod.fst) =O[l ×ˢ l'] (g ∘ Prod.fst)

Tactic:
by
  simp only [isBigO_iff, eventually_prod_iff]
  exact fun ⟨c, hc⟩ ↦ ⟨c, _, hc, fun _ ↦ True, eventually_true l', fun {_} h {_} _ ↦ h⟩

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 : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
j : ℕ
⊢ j ≥ max n i → abv ((fun n ↦ ∑ i ∈ range n, f i) j - (fun n ↦ ∑ i ∈ range n, f i) (max n i)) < ε

Tactic:
ji

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
hg : IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
j : ℕ
ji : j ≥ max n i
⊢ abv ((fun n ↦ ∑ i ∈ range n, f i) j - (fun n ↦ ∑ i ∈ range n, f i) (max n i)) < ε
Module: Mathlib.Analysis.Normed.Operator.LinearIsometry

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁴ : RingHomInvPair σ₂₁ σ₁₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup E₂
inst✝¹ : Module R E
inst✝ : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ range ⇑e = univ

Tactic:
by
  rw [← coe_toIsometryEquiv]
  exact IsometryEquiv.range_eq_univ _

Goal state after:
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
g : α → F
s : Set α
⊢ f =O[𝓟 s] g ↔ ∃ c, ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖

Tactic:
by
  simp_rw [isBigO_iff, eventually_principal]

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

Goal state before:
pp: α : Type u_1
F : Type u_4
E''' : Type u_12
inst✝³ : Norm F
inst✝² : SeminormedAddGroup E'''
l : Filter α
inst✝¹ : One F
inst✝ : NormOneClass F
f : α → E'''
⊢ (f =o[l] fun _x ↦ 1) ↔ Tendsto f l (𝓝 0)

Tactic:
simp only [isLittleO_iff, norm_one, mul_one, Metric.nhds_basis_closedBall.tendsto_right_iff,
    Metric.mem_closedBall, dist_zero_right]

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
B : ι → α → ℝ
hAB : ∀ i ∈ s, A i =o[l] B i
⊢ (fun H ↦ ∑ i ∈ s, A i H) =o[l] fun H ↦ ∑ i ∈ s, ‖B i H‖

Tactic:
induction s using Finset.cons_induction with
  | empty => simp [isLittleO_zero]
  | cons i s his h =>
  simp_rw [Finset.sum_cons]
  calc (fun H => A i H + ∑ j ∈ s, A j H)
      =o[l] fun H => ‖B i H‖ + ‖∑ j ∈ s, ‖B j H‖‖ :=
          (hAB i (by simp)).add_add (h (fun j hj => hAB j (by simp [hj])))
    _ =ᶠ[l] fun H => ‖B i H‖ + ∑ j ∈ s, ‖B j H‖ := by
        refine Eventually.of_forall fun H ↦ congr_arg (‖B i H‖ + ·) ?_
        exact Real.norm_of_nonneg (Finset.sum_nonneg fun _ _ => norm_nonneg _)

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

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

Tactic:
refine Finset.sum_congr rfl fun m _ => ?_

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

Goal state before:
pp: x y : ℂ
s1 : sin ((x + x + y - y) / 2) = sin ((x + y) / 2) * cos ((x - y) / 2) + cos ((x + y) / 2) * sin ((x - y) / 2)
s2 : sin ((x + y) / 2 - (x - y) / 2) = sin ((x + y) / 2) * cos ((x - y) / 2) - cos ((x + y) / 2) * sin ((x - y) / 2)
⊢ sin x - sin y = 2 * sin ((x - y) / 2) * cos ((x + y) / 2)

Tactic:
add_sub_cancel_right,

Goal state after:
x y : ℂ
s1 : sin ((x + x) / 2) = sin ((x + y) / 2) * cos ((x - y) / 2) + cos ((x + y) / 2) * sin ((x - y) / 2)
s2 : sin ((x + y) / 2 - (x - y) / 2) = sin ((x + y) / 2) * cos ((x - y) / 2) - cos ((x + y) / 2) * sin ((x - y) / 2)
⊢ sin x - sin y = 2 * sin ((x - y) / 2) * cos ((x + y) / 2)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
s1 : cos ((x + x + y - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)
s2 : cos ((x + y) / 2 - (x - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)
⊢ cos x - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2)

Tactic:
add_sub_cancel_right,

Goal state after:
x y : ℂ
s1 : cos ((x + x) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)
s2 : cos ((x + y) / 2 - (x - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)
⊢ cos x - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cos x ^ 2 + sin x ^ 2 = 1

Tactic:
by rw [add_comm, sin_sq_add_cos_sq]

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

Goal state before:
pp: x : ℝ
⊢ cos x ^ 2 + sin x ^ 2 = 1

Tactic:
by rw [add_comm, sin_sq_add_cos_sq]

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

Goal state before:
pp: x : ℝ
⊢ cosh x * 2 = rexp x + rexp (-x)

Tactic:
by
    rw [cosh, exp, exp, Complex.ofReal_neg, Complex.cosh, mul_two, ← Complex.add_re, ← mul_two,
      div_mul_cancel₀ _ (two_ne_zero' ℂ), Complex.add_re]

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
k : ℤ
⊢ a ≠ 0 ∨ k + k ≠ 0 ∨ k = 0 ∧ k = 0

Tactic:
by simp [em']

Goal state after:
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
k : ℤ
h : k + k ≠ 0
⊢ a ≠ 0 ∨ k + k ≠ 0 ∨ k = 0 ∧ k = 0

Tactic:
by simp [em']

Goal state after:
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
s : Finset ι × Finset ι' → Finset (ι × ι') := fun p ↦ p.1 ×ˢ p.2
this :
  Tendsto (Prod.map (fun s ↦ ∑ b ∈ s, f b) fun s ↦ ∑ b ∈ s, g b)
    ((SummationFilter.unconditional ι).filter ×ˢ (SummationFilter.unconditional ι').filter)
    (𝓝 (∑' (b : ι), f b) ×ˢ 𝓝 (∑' (b : ι'), g b))
⊢ Tendsto (fun b ↦ ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2) (atTop ×ˢ atTop) (𝓝 ((∑' (i : ι), f i) * ∑' (j : ι'), g j))

Tactic:
rw [← nhds_prod_eq] at this

Goal state after:
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
s : Finset ι × Finset ι' → Finset (ι × ι') := fun p ↦ p.1 ×ˢ p.2
this :
  Tendsto (Prod.map (fun s ↦ ∑ b ∈ s, f b) fun s ↦ ∑ b ∈ s, g b)
    ((SummationFilter.unconditional ι).filter ×ˢ (SummationFilter.unconditional ι').filter)
    (𝓝 (∑' (b : ι), f b, ∑' (b : ι'), g b))
⊢ Tendsto (fun b ↦ ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2) (atTop ×ˢ atTop) (𝓝 ((∑' (i : ι), f i) * ∑' (j : ι'), g j))
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ ball (x / 1) δ = ball x δ

Tactic:
div_one

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ ball x δ = ball x δ
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ closedBall (x / 1) δ = closedBall x δ

Tactic:
div_one

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ closedBall x δ = closedBall 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
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, f x = 0
x : M ⧸ S
x✝ : ‖f‖ = 0 ∨ 0 < ‖f‖
⊢ ‖(lift S f.toAddMonoidHom hf) x‖ ≤ ‖f‖ * ‖x‖

Tactic:
cases (norm_nonneg f).eq_or_lt' with

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ {x} / sphere 1 δ = sphere x δ

Tactic:
singleton_div_sphere,

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ sphere (x / 1) δ = sphere x δ
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ sphere (x / 1) δ = sphere x δ

Tactic:
div_one

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ sphere x δ = sphere x δ
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
x : E
⊢ s / ball x δ = x⁻¹ • thickening δ s

Tactic:
by simp [div_eq_mul_inv]

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
x : E
⊢ ball x δ / s = x • thickening δ s⁻¹

Tactic:
by simp [div_eq_mul_inv]

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 : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
⊢ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r)

Tactic:
have : ContinuousWithinAt (fun c : ℝ => c • (y - x) + x) (Ico 0 1) 1 := by fun_prop

Goal state after:
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 ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x r)
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case convert_3
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
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
⊢ ‖(fun c ↦ c • (y - x) + x) c - x‖ < r

Tactic:
add_sub_cancel_right,

Goal state after:
case convert_3
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
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
⊢ ‖c • (y - x)‖ < 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 • ball x r = ball (c • x) (‖c‖ * r)

Tactic:
ext y
  rw [mem_smul_set_iff_inv_smul_mem₀ hc]
  conv_lhs => rw [← inv_smul_smul₀ hc x]
  simp [← div_eq_inv_mul, div_lt_iff₀ (norm_pos_iff.2 hc), mul_comm _ r, dist_smul₀]

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

Goal state before:
pp: θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
⊢ 4 * c ^ 2 - 2 * c - 1 = 0

Tactic:
set s := sin θ

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

Goal state before:
pp: θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
⊢ s ≠ 0

Tactic:
ne_eq,

Goal state after:
θ : ℝ := π / 5
hθ : θ = π / 5
c : ℝ := cos θ
s : ℝ := sin θ
⊢ ¬s = 0
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 < δ
s : Set E
x : E
⊢ infEDist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ → infEDist x s - ENNReal.ofReal δ ≤ ENNReal.ofReal ε

Tactic:
exact tsub_le_iff_right.2

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 ≤ δ
s : Set E
x : E
⊢ infEDist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ → infEDist x s - ENNReal.ofReal δ ≤ ENNReal.ofReal ε

Tactic:
exact tsub_le_iff_right.2

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

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
k✝ : ℕ
r : R
hr : ‖r‖ < 1
k : ℕ
hk : ∀ m < k, Summable fun n ↦ ↑n ^ m * r ^ n
P : ℕ[X] := (ascPochhammer ℕ k).comp (X + C 1)
n : ℕ
mP : P.Monic
⊢ P.natDegree = k

Tactic:
simp only [P, natDegree_comp, ascPochhammer_natDegree, mul_one, natDegree_X_add_C]

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
⊢ Continuous uncurry

Tactic:
by
  apply continuous_of_continuous_uncurry
  rw [← (Homeomorph.prodAssoc _ _ _).comp_continuous_iff']
  dsimp [Function.comp_def]
  exact (continuous_fst.fst.eval continuous_fst.snd).eval continuous_snd

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

Goal state before:
pp: case inr
p x ε : ℝ
hp : p ≠ 0
y : ℝ
⊢ (∃ i, |y - x - ↑i * p| ≤ ε) → |y - x - ↑(round (p⁻¹ * (y - x))) * p| ≤ ε

Tactic:
rintro ⟨n, hn⟩

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