mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: s s₁ t t₁ : Set ℝ
⊢ s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁

Tactic:
rw [← @preimage_equivRealProd_prod s t, ← @preimage_equivRealProd_prod s₁ t₁]

Goal state after:
s s₁ t t₁ : Set ℝ
⊢ ⇑equivRealProd ⁻¹' s ×ˢ t ⊆ ⇑equivRealProd ⁻¹' s₁ ×ˢ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝² : SFinite ν
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
⊢ μ.prod (c • ν) = c • μ.prod ν

Tactic:
ext s hs

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝² : SFinite ν
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
s : Set (α × β)
hs : MeasurableSet s
⊢ (μ.prod (c • ν)) s = (c • μ.prod ν) s
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
⊢ (algebraMap ℝ A) 1 + 0 • I' = 1

Tactic:
map_one,

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
⊢ 1 + 0 • I' = 1
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: f : ℂ →+* ℂ
hf : Continuous ⇑f
⊢ f = RingHom.id ℂ ∨ f = starRingEnd ℂ

Tactic:
simpa only [DFunLike.ext_iff] using! real_algHom_eq_id_or_conj (AlgHom.mk' f (map_real_smul f hf))

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

Goal state before:
pp: case inl
𝕜 : Type u_2
inst✝ : RCLike 𝕜
a : 𝕜
h : RCLike.I = 0
⊢ ‖↑(RCLike.re a) + ↑(RCLike.im a) * I‖ = ‖a‖

pp: case inr
𝕜 : Type u_2
inst✝ : RCLike 𝕜
a : 𝕜
h : RCLike.im RCLike.I = 1
⊢ ‖↑(RCLike.re a) + ↑(RCLike.im a) * I‖ = ‖a‖

Tactic:
· rw [← RCLike.re_add_im a, RCLike.im_eq_zero h]
    simp

Goal state after:
case inr
𝕜 : Type u_2
inst✝ : RCLike 𝕜
a : 𝕜
h : RCLike.im RCLike.I = 1
⊢ ‖↑(RCLike.re a) + ↑(RCLike.im a) * I‖ = ‖a‖
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
y : ℝ
hx : IsSelfAdjoint x
⊢ y = re x ↔ ↑y = x

Tactic:
by
  simpa [eq_comm] using re_eq_ofReal_of_isSelfAdjoint hx

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 < normSq z ↔ z ≠ 0

Tactic:
rw [lt_iff_le_and_ne, Ne, eq_comm]; simp [normSq_nonneg]

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

Goal state before:
pp: r : ℝ
⊢ ℑ ↑r = 0

Tactic:
ext1

Goal state after:
r : ℝ
⊢ ↑(ℑ ↑r) = ↑0
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
r : ℝ
⊢ re (z / ↑r) = re z / r

Tactic:
div_eq_inv_mul,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
r : ℝ
⊢ re ((↑r)⁻¹ * z) = re z / r
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
r : ℝ
⊢ re ((↑r)⁻¹ * z) = re z / r

Tactic:
div_eq_inv_mul,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
r : ℝ
⊢ re ((↑r)⁻¹ * z) = r⁻¹ * re z
Module: Mathlib.Analysis.Asymptotics.Theta

Goal state before:
pp: α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : (fun x ↦ (f x)⁻¹) =Θ[l] fun x ↦ (g x)⁻¹
⊢ f =Θ[l] g

Tactic:
simpa only [inv_inv] using h.inv

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

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
l : Filter α
⊢ f =o[l] g ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g

Tactic:
rw [IsLittleO_def]

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ f₁ =o[l] g₁ ↔ f₂ =o[l] g₂

Tactic:
by
  simp only [IsLittleO_def]
  exact forall₂_congr fun c _hc => isBigOWith_congr (Eq.refl c) hf hg

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
f' : α → E'
l : Filter α
h : ∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0
⊢ ¬f' =o[l] f'

Tactic:
intro ho
  rcases ((ho.bound one_half_pos).and_frequently h).exists with ⟨x, hle, hne⟩
  rw [one_div, ← div_eq_inv_mul] at hle
  exact (half_lt_self (lt_of_le_of_ne (norm_nonneg _) hne.symm)).not_ge hle

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
c : ℝ
f : α → E
g' : α → F'
l : Filter α
⊢ (IsBigOWith c l f fun x ↦ -g' x) ↔ IsBigOWith c l f g'

Tactic:
by
  simp only [IsBigOWith_def, norm_neg]

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

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
c : ℝ
g : α → F
f' : α → E'
l : Filter α
⊢ IsBigOWith c l (fun x ↦ -f' x) g ↔ IsBigOWith c l f' g

Tactic:
by
  simp only [IsBigOWith_def, norm_neg]

Goal state after:
Module: Mathlib.Tactic.NormNum.NatFactorial

Goal state before:
pp: n x l y z : ℕ
h₁ : IsNat n x
h₂ : IsNat l y
h₃ : y = z + x + 1
⊢ n.descFactorial l = ↑0

Tactic:
simp [h₁.out, h₂.out, h₃]

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

Goal state before:
pp: case e'_7
α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f : α → R
g : α → S
h : f =o[l] g
n : ℕ
ihn : (fun x ↦ f x ^ n.succ) =o[l] fun x ↦ g x ^ n.succ
x✝ : α
⊢ f x✝ ^ (n + 1).succ = f x✝ ^ n.succ * f x✝

Tactic:
simp [pow_succ]

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

Goal state before:
pp: case e'_8
α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f : α → R
g : α → S
h : f =o[l] g
n : ℕ
ihn : (fun x ↦ f x ^ n.succ) =o[l] fun x ↦ g x ^ n.succ
x✝ : α
⊢ g x✝ ^ (n + 1).succ = g x✝ ^ n.succ * g x✝

Tactic:
simp [pow_succ]

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

Goal state before:
pp: z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ |‖z ^ m.succ / ↑m.succ.factorial‖| ≤ ‖z‖ / ↑n * |‖z ^ m / ↑m.factorial‖|

Tactic:
rw [abs_norm, abs_norm, Nat.factorial_succ, pow_succ', mul_comm m.succ, Nat.cast_mul,
        ← div_div, mul_div_assoc, mul_div_right_comm, Complex.norm_mul, Complex.norm_div,
        norm_natCast]

Goal state after:
z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ ‖z‖ / ↑m.succ * ‖z ^ m / ↑m.factorial‖ ≤ ‖z‖ / ↑n * ‖z ^ m / ↑m.factorial‖
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'
B : ι → α → ℝ
C : ℝ
i : α → Finset ι
hAB : ∀ᶠ (x : ι × α) in ⊤ ×ˢ l, ‖Function.uncurry A x‖ ≤ C * ‖Function.uncurry B x‖
s₁ : ι → Prop
hs₁ : ∀ᶠ (x : ι) in ⊤, s₁ x
s₂ : α → Prop
hs₂ : ∀ᶠ (y : α) in l, s₂ y
hbound : ∀ {x : ι}, s₁ x → ∀ {y : α}, s₂ y → ‖Function.uncurry A (x, y)‖ ≤ C * ‖Function.uncurry B (x, y)‖
H : α
hH : s₂ H
⊢ C * ∑ j ∈ i H, ‖B j H‖ = C * ‖∑ j ∈ i H, ‖B j H‖‖

Tactic:
by
        congr; rw [Real.norm_of_nonneg (Finset.sum_nonneg (fun _ _ ↦ norm_nonneg _))]

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

Goal state before:
pp: x : ℂ
⊢ tan (x * I) = tanh x * I

Tactic:
tan,

Goal state after:
x : ℂ
⊢ sin (x * I) / cos (x * I) = tanh x * I
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : E'' → F''
x₀ : E''
n : ℕ
h : f =O[𝓝 x₀] fun x ↦ ‖x - x₀‖ ^ n
hn : n ≠ 0
⊢ f x₀ = 0

Tactic:
← nhdsWithin_univ

Goal state after:
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : E'' → F''
x₀ : E''
n : ℕ
h : f =O[𝓝[univ] x₀] fun x ↦ ‖x - x₀‖ ^ n
hn : n ≠ 0
⊢ f x₀ = 0
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ tan ((starRingEnd ℂ) x) = (starRingEnd ℂ) (tan x)

Tactic:
tan,

Goal state after:
x : ℂ
⊢ sin ((starRingEnd ℂ) x) / cos ((starRingEnd ℂ) x) = (starRingEnd ℂ) (tan x)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ tan ((starRingEnd ℂ) x) = (starRingEnd ℂ) (tan x)

Tactic:
rw [tan, sin_conj, cos_conj, ← map_div₀, tan]

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

Goal state before:
pp: x : ℂ
n : ℕ
⊢ ‖cexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial‖ ≤ Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / ↑m.factorial

Tactic:
rw [← CauSeq.lim_const (abv := norm) (∑ m ∈ range n, _), Complex.exp, sub_eq_add_neg,
    ← CauSeq.lim_neg, CauSeq.lim_add, ← lim_norm]

Goal state after:
x : ℂ
n : ℕ
⊢ (cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / ↑m.factorial))).lim ≤
    Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / ↑m.factorial
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n : ℕ
⊢ ‖cexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial‖ ≤ ‖x‖ ^ n * Real.exp ‖x‖

Tactic:
rw [← CauSeq.lim_const (abv := norm) (∑ m ∈ range n, _), Complex.exp, sub_eq_add_neg,
    ← CauSeq.lim_neg, CauSeq.lim_add, ← lim_norm]

Goal state after:
x : ℂ
n : ℕ
⊢ (cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / ↑m.factorial))).lim ≤ ‖x‖ ^ n * Real.exp ‖x‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case hbc
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ 0 ≤ ‖x‖

Tactic:
exact norm_nonneg _

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

Goal state before:
pp: x : ℝ
hx : |x| ≤ 1
⊢ |cos x - (1 - x ^ 2 / 2)| ≤ |x| ^ 4 * (5 / 96)

Tactic:
by
  simpa [← ofReal_cos, ← norm_eq_abs, ← norm_real] using Complex.cos_bound (x := x) (by simpa)

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

Goal state before:
pp: case hab
x : ℝ
hx : |x| ≤ 1
⊢ x * x ≤ 1

Tactic:
← abs_mul_self,

Goal state after:
case hab
x : ℝ
hx : |x| ≤ 1
⊢ |x * x| ≤ 1
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:
rw [Classical.not_imp, not_lt] at hi

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 ∧ f i ≤ a - (Nat.find h).pred • ε
⊢ ∃ i, ∀ j ≥ i, |f j - f i| < ε
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: case inl.inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
s : Set E
hs : s.Nonempty
⊢ ‖0‖₊ • ediam s ≤ ediam (0 • s)

Tactic:
simp [zero_smul_set hs, ← Set.singleton_zero]

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
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (closedBall x r) \ interior (closedBall x r) = sphere x r

Tactic:
closure_closedBall,

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ closedBall x r \ interior (closedBall x r) = sphere x r
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (closedBall x r) \ interior (closedBall x r) = sphere x r

Tactic:
closure_closedBall,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ closedBall x r \ interior (closedBall x r) = sphere x r
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 4) = √2 / 2

Tactic:
trans sin (π / 2 ^ 2)
  · congr
    norm_num
  · simp

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

Goal state before:
pp: ⊢ cos (π / 8) = √(2 + √2) / 2

Tactic:
by
  trans cos (π / 2 ^ 3)
  · congr
    norm_num
  · simp

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

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

Tactic:
rw [← cos_pi_div_two_sub, ← cos_pi_div_six]

Goal state after:
⊢ cos (π / 2 - π / 3) = cos (π / 6)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
⊢ r • closedBall 0 1 = closedBall 0 r

Tactic:
by
  rw [smul_unitClosedBall, Real.norm_of_nonneg hr]

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case refine_1
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : s ∈ 𝓝 (const X c)
S : Set (Set X × Set Y)
hSf : S.Finite
hSsub : {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst✝] U
hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c)) K U
this : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c
i : ι
hpi : p i
hi : U i ⊆ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2
⊢ {f | MapsTo ⇑f (⋃ KU ∈ S, KU.1, i).1 (U (⋃ KU ∈ S, KU.1, i).2)} ⊆
    {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g) K U}

Tactic:
intro f hf K V hKV

Goal state after:
case refine_1
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : s ∈ 𝓝 (const X c)
S : Set (Set X × Set Y)
hSf : S.Finite
hSsub : {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst✝] U
hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c)) K U
this : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c
i : ι
hpi : p i
hi : U i ⊆ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2
f : C(X, Y)
hf : f ∈ {f | MapsTo ⇑f (⋃ KU ∈ S, KU.1, i).1 (U (⋃ KU ∈ S, KU.1, i).2)}
K : Set X
V : Set Y
hKV : (K, V) ∈ S
⊢ MapsTo (⇑f) K V
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
r : X
f : C(Y, Z)
K : Set Y
hK : IsCompact K
U : Set (X × Z)
hU : IsOpen[instTopologicalSpaceProd] U
H : MapsTo (⇑((const Y (r, f).1).prodMk (r, f).2)) K U
⊢ {r} ×ˢ (⇑f '' K) ⊆ U

Tactic:
simpa [Set.subset_def, forall_comm (α := X)]

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

Goal state before:
pp: α : Type u_4
inst✝¹ : SeminormedAddCommGroup α
inst✝ : CompleteSpace α
f : ℕ → α
r : ℝ
hr₁ : r < 1
h✝ : ∀ᶠ (n : ℕ) in atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖
hr₀ : r < 0
a✝ : ℕ
hn : ‖f (a✝ + 1)‖ ≤ r * ‖f a✝‖
h : 0 < ‖f a✝‖
⊢ False

Tactic:
exact not_lt.mpr (norm_nonneg _) (lt_of_le_of_lt hn <| mul_neg_of_neg_of_pos hr₀ h)

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

Goal state before:
pp: case right
X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
⊢ ∀ ⦃y : X⦄, y ∈ U ∪ V → JoinedIn (U ∪ V) x y

Tactic:
rintro y (yU | yV)

Goal state after:
case right.inl
X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
y : X
yU : y ∈ U
⊢ JoinedIn (U ∪ V) x y

case right.inr
X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
y : X
yV : y ∈ V
⊢ JoinedIn (U ∪ V) x y
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case snoc.snoc
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
n : ℕ
p : Fin n → X
y x : X
hx : x ∈ s
hp : ∀ (i : Fin n), p i ∈ s
hy : y ∈ s
γ₀ : Path (snoc p y 0) y
hγ₀s : range ⇑γ₀ ⊆ s
hγ₀p : ∀ (i : Fin n), p i ∈ range ⇑γ₀
⊢ ∃ γ, range ⇑γ ⊆ s ∧ (∀ (i : Fin n), p i ∈ range ⇑γ) ∧ y ∈ range ⇑γ

Tactic:
obtain ⟨γ₁, hγ₁⟩ := h.joinedIn y hy x hx

Goal state after:
case snoc.snoc
X : Type u_1
inst✝ : TopologicalSpace X
n✝ : ℕ
s : Set X
h : IsPathConnected s
n : ℕ
p : Fin n → X
y x : X
hx : x ∈ s
hp : ∀ (i : Fin n), p i ∈ s
hy : y ∈ s
γ₀ : Path (snoc p y 0) y
hγ₀s : range ⇑γ₀ ⊆ s
hγ₀p : ∀ (i : Fin n), p i ∈ range ⇑γ₀
γ₁ : Path y x
hγ₁ : ∀ (t : ↑I), γ₁ t ∈ s
⊢ ∃ γ, range ⇑γ ⊆ s ∧ (∀ (i : Fin n), p i ∈ range ⇑γ) ∧ y ∈ range ⇑γ
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
p : Fin (n + 1) → X
hp : ∀ (i : Fin (n + 1)), p i ∈ s
⊢ ∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ

Tactic:
by
  cases p using snocCases with | _ p x => ?_
  simp only [forall_fin_succ', snoc_castSucc, snoc_last, Path.cast_coe,
    Path.target_mem_range, and_true] at hp ⊢
  obtain ⟨hp, hx⟩ := hp
  induction p using snocInduction generalizing x with
  | elim0 =>
    simp only [snoc_zero]
    use Path.refl x
    simp [hx]
  | @snoc n p y hp₂ =>
    simp only [forall_fin_succ', snoc_castSucc, snoc_last, snoc_apply_zero, Path.cast_coe] at hp ⊢
    obtain ⟨hp, hy⟩ := hp
    specialize hp₂ y hp hy
    obtain ⟨γ₀, hγ₀s, hγ₀p⟩ := hp₂
    obtain ⟨γ₁, hγ₁⟩ := h.joinedIn y hy x hx
    rw [← range_subset_iff] at hγ₁
    use γ₀.trans γ₁
    simp only [Path.trans_range, mem_union, Path.source_mem_range, or_true, and_true,
      union_subset_iff]
    tauto

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: case mpr
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
⊢ (∀ (s : Set X), IsCompact s → ∃ f, Tendsto (fun i ↦ restrict s (F i)) l (𝓝 f)) → ∃ f, Tendsto F l (𝓝 f)

Tactic:
intro h
    choose f hf using h
    -- By uniqueness of limits in a `T2Space`, since `fun i ↦ F i x` tends to both `f s₁ hs₁ x` and
    -- `f s₂ hs₂ x`, we have `f s₁ hs₁ x = f s₂ hs₂ x`
    have h :
      ∀ (s₁) (hs₁ : IsCompact s₁) (s₂) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
        f s₁ hs₁ ⟨x, hxs₁⟩ = f s₂ hs₂ ⟨x, hxs₂⟩ := by
      rintro s₁ hs₁ s₂ hs₂ x hxs₁ hxs₂
      have := isCompact_iff_compactSpace.mp hs₁
      have := isCompact_iff_compactSpace.mp hs₂
      have h₁ := (continuous_eval_const (⟨x, hxs₁⟩ : s₁)).continuousAt.tendsto.comp (hf s₁ hs₁)
      have h₂ := (continuous_eval_const (⟨x, hxs₂⟩ : s₂)).continuousAt.tendsto.comp (hf s₂ hs₂)
      exact tendsto_nhds_unique h₁ h₂
    -- So glue the `f s hs` together and prove that this glued function `f₀` is a limit on each
    -- compact set `s`
    refine ⟨liftCover' _ _ h exists_compact_mem_nhds, ?_⟩
    rw [tendsto_compactOpen_iff_forall]
    intro s hs
    rw [liftCover_restrict']
    exact hf s hs

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

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := ⋯
⊢ PathConnectedSpace X → Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)

Tactic:
intro h
    refine ⟨(nonempty_quotient_iff _).mpr h.1, ⟨?_⟩⟩
    rintro ⟨x⟩ ⟨y⟩
    exact Quotient.sound (PathConnectedSpace.joined x y)

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
this : IsPathConnected univ
γ : Path (p 0) (p (last n))
h : ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ
⊢ ∃ γ, ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ

Tactic:
exact ⟨γ, h⟩

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ g (f p.1, p.2)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] g

Tactic:
let Gf : C(X₀, C(Y, Z)) := ContinuousMap.curry ⟨_, hg⟩

Goal state after:
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : IsQuotientMap f
g : X × Y → Z
hg : Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ g (f p.1, p.2)
Gf : C(X₀, C(Y, Z)) := { toFun := fun p ↦ g (f p.1, p.2), continuous_toFun := hg }.curry
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] g
Module: Mathlib.Topology.Instances.AddCircle.Real

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : x.val = y.val
this : 0 < ↑N
⊢ x = y

pp: case hx
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ↑x.val / ↑N ∈ Ico ?m.62 (?m.62 + 1)

pp: case hy
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ↑y.val / ↑N ∈ Ico ?m.62 (?m.62 + 1)

pp: N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ℝ

Tactic:
(val_injective N).eq_iff

Goal state after:
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : x = y
this : 0 < ↑N
⊢ x = y

case hx
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ↑x.val / ↑N ∈ Ico ?m.62 (?m.62 + 1)

case hy
N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ↑y.val / ↑N ∈ Ico ?m.62 (?m.62 + 1)

N : ℕ
inst✝ : NeZero N
x y : ZMod N
hxy : ↑(↑x.val / ↑N) = ↑(↑y.val / ↑N)
this : 0 < ↑N
⊢ ℝ
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
hx : |p| * ‖↑(p⁻¹ * x)‖ = ‖↑x‖
⊢ |p * (p⁻¹ * x) - p * ↑(round (p⁻¹ * x))| = |x - ↑(round (p⁻¹ * x)) * p|

Tactic:
mul_inv_cancel_left₀ hp,

Goal state after:
case inr
p x : ℝ
this : ∀ (x : ℝ), ‖↑x‖ = |x - ↑(round x)|
hp : p ≠ 0
hx : |p| * ‖↑(p⁻¹ * x)‖ = ‖↑x‖
⊢ |x - p * ↑(round (p⁻¹ * x))| = |x - ↑(round (p⁻¹ * x)) * p|
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case mk
p : ℝ
x✝ : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ |p⁻¹ * x - ↑(round (p⁻¹ * x))| ≤ 1 / 2

Tactic:
exact abs_sub_round (p⁻¹ * x)

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

Goal state before:
pp: E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x + (-1) ^ (2 * n) * f (2 * n) + -1 * (-1) ^ (2 * n) * f (2 * n + 1) ≤
    ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x

Tactic:
show (-1 : E) ^ (2 * n) = 1 by simp,

Goal state after:
E : Type u_4
inst✝⁴ : Ring E
inst✝³ : PartialOrder E
inst✝² : IsOrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfm : Monotone f
k n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x + 1 * f (2 * n) + -1 * 1 * f (2 * n + 1) ≤
    ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x