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

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C C' : ℝ
h : f.SurjectiveOnWith K C
H : C ≤ C'
⊢ f.SurjectiveOnWith K C'

Tactic:
intro k k_in

Goal state after:
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C C' : ℝ
h : f.SurjectiveOnWith K C
H : C ≤ C'
k : V₂
k_in : k ∈ K
⊢ ∃ g, f g = k ∧ ‖g‖ ≤ C' * ‖k‖
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
inst✝¹ : SeminormedAddCommGroup V
inst✝ : NontrivialTopology V
⊢ 1 ≤ ‖id V‖

Tactic:
let ⟨x, hx⟩ := exists_norm_ne_zero V

Goal state after:
V : Type u_1
inst✝¹ : SeminormedAddCommGroup V
inst✝ : NontrivialTopology V
x : V
hx : ‖x‖ ≠ 0
⊢ 1 ≤ ‖id V‖
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f g : NormedAddGroupHom V W
x : ↥(f.equalizer g)
⊢ f ((ι f g) x) - g ((ι f g) x) = 0

Tactic:
← NormedAddGroupHom.sub_apply

Goal state after:
V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f g : NormedAddGroupHom V W
x : ↥(f.equalizer g)
⊢ (f - g) ((ι f g) x) = 0
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: α : 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 : γ
⊢ ∑'[L] (i : β), g • f i = g • ∑'[L] (i : β), f i

Tactic:
by
  rcases eq_or_ne g 0 with rfl | hg
  · simp
  · exact tsum_const_smul' (Units.mk0 g hg)

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

Goal state before:
pp: ⊢ LipschitzWith 1 ⇑equivRealProd

Tactic:
simpa using! AddMonoidHomClass.lipschitz_of_bound equivRealProdLm 1 equivRealProd_apply_le'

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

Goal state before:
pp: A : Type u_1
inst✝⁴ : SeminormedAddCommGroup A
inst✝³ : StarAddMonoid A
inst✝² : NormedSpace ℂ A
inst✝¹ : StarModule ℂ A
inst✝ : NormedStarGroup A
x : A
⊢ ‖realPart x‖ ≤ ‖x‖

Tactic:
by
  rw [← inv_mul_cancel_left₀ two_ne_zero ‖x‖, ← AddSubgroup.norm_coe, realPart_apply_coe,
    norm_smul, norm_inv, Real.norm_ofNat]
  gcongr
  exact norm_add_le _ _ |>.trans <| by simp [two_mul]

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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (z : 𝕜),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          re)
        ((starRingEnd 𝕜) z) =
      (⋯ ▸
          let __spread.0 := h.toNormedField;
          re)
        z

Tactic:
by subst h''; exact h.conj_re_ax

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, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
by
  simp only [IsBigO_def, IsBigOWith_def]

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₁ c₂ : ℝ
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : IsBigOWith c₁ l f₁ g
h₂ : f₂ =o[l] g
hc : c₁ < c₂
⊢ IsBigOWith c₂ l (fun x ↦ f₁ x - f₂ x) g

Tactic:
simpa only [sub_eq_add_neg] using h₁.add_isLittleO h₂.neg_left hc

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

Goal state before:
pp: case cons
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s✝ : Finset ι
i : ι
s : Finset ι
is : i ∉ s
IH : (∀ i ∈ s, IsBigOWith (C i) l (A i) g) → IsBigOWith (∑ i ∈ s, C i) l (∑ i ∈ s, A i) g
h : ∀ i_1 ∈ Finset.cons i s is, IsBigOWith (C i_1) l (A i_1) g
⊢ IsBigOWith (∑ i ∈ Finset.cons i s is, C i) l (∑ i ∈ Finset.cons i s is, A i) g

Tactic:
| cons i s is IH =>

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

Goal state before:
pp: x : ℂ
⊢ cosh x + sinh x = cexp x

Tactic:
rw [← mul_right_inj' (two_ne_zero' ℂ), mul_add, two_cosh, two_sinh, add_add_sub_cancel, two_mul]

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

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

Tactic:
by
  rw [← cosh_mul_I, add_mul, cosh_add, cosh_mul_I, cosh_mul_I, sinh_mul_I, sinh_mul_I,
    mul_mul_mul_comm, I_mul_I, mul_neg_one, sub_eq_add_neg]

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

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
m : ℕ
hm : m ∈ {m ∈ range j | n ≤ m}
⊢ x ^ m / ↑m.factorial = x ^ n * (x ^ (m - n) / ↑m.factorial)

Tactic:
mem_filter,

Goal state after:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
m : ℕ
hm : m ∈ range j ∧ n ≤ m
⊢ x ^ m / ↑m.factorial = x ^ n * (x ^ (m - n) / ↑m.factorial)
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''
g : ℕ → F''
hfg : f =O[atTop] g
l : Filter ℕ
h : ∀ᶠ (n : ℕ) in l, g n = 0 → f n = 0
C : ℝ
hC_pos : C > 0
hC : ∀ ⦃x : ℕ⦄, g x ≠ 0 → ‖f x‖ ≤ C * ‖g x‖
⊢ f =O[l] g

Tactic:
refine isBigO_iff.mpr ⟨C, ?_⟩

Goal state after:
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
hfg : f =O[atTop] g
l : Filter ℕ
h : ∀ᶠ (n : ℕ) in l, g n = 0 → f n = 0
C : ℝ
hC_pos : C > 0
hC : ∀ ⦃x : ℕ⦄, g x ≠ 0 → ‖f x‖ ≤ C * ‖g x‖
⊢ ∀ᶠ (x : ℕ) in l, ‖f x‖ ≤ C * ‖g x‖
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖x‖ ^ 2 * 1 = ‖x‖ ^ 2

Tactic:
mul_one

Goal state after:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖x‖ ^ 2 = ‖x‖ ^ 2
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖∑ k ∈ Ico n j, x ^ k / ↑k.factorial‖ ≤ ↑(const abs (‖x‖ ^ n * Real.exp ‖x‖)) j

Tactic:
calc
    ‖∑ m ∈ Ico n j, (x ^ m / m.factorial : ℂ)‖
      = ‖∑ m ∈ Ico n j, (x ^ n * (x ^ (m - n) / m.factorial) : ℂ)‖ := by
      refine congr_arg norm (sum_congr rfl fun m hm => ?_)
      rw [mem_Ico] at hm
      rw [← mul_div_assoc, ← pow_add, add_tsub_cancel_of_le hm.1]
    _ ≤ ∑ m ∈ Ico n j, ‖x ^ n * (x ^ (m - n) / m.factorial)‖ :=
      IsAbsoluteValue.abv_sum norm ..
    _ ≤ ∑ m ∈ Ico n j, ‖x‖ ^ n * (‖x‖ ^ (m - n) / (m - n).factorial) := by
      simp_rw [Complex.norm_mul, Complex.norm_pow, Complex.norm_div, norm_natCast]
      gcongr with i hi
      · rw [Complex.norm_pow]
      · simp
    _ = ‖x‖ ^ n * ∑ m ∈ range (j - n), (‖x‖ ^ m / m.factorial) := by
      simp [← mul_sum, sum_Ico_eq_sum_range]
    _ ≤ ‖x‖ ^ n * Real.exp ‖x‖ := by
      gcongr
      refine Real.sum_le_exp_of_nonneg ?_ _
      exact norm_nonneg _

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

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

Tactic:
by simp [sin_sq_add_cos_sq]

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

Goal state before:
pp: z : ℂ
⊢ Real.exp z.re * 1 = Real.exp z.re

Tactic:
mul_one

Goal state after:
z : ℂ
⊢ Real.exp z.re = Real.exp z.re
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: case inr
x : ℝ
hx : 0 ≤ x
hx' : x < 2
hx₀ : 0 < x
⊢ rexp x ≤ (2 + x) / (2 - x)

Tactic:
exact (exp_lt_two_add_div_two_sub hx₀ hx').le

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: α : Type u_1
l : Filter α
f : ℝ → α
⊢ Tendsto (fun x ↦ f (rexp x)) atBot l ↔ Tendsto f (𝓝[>] 0) l

Tactic:
by
  rw [← map_exp_atBot, tendsto_map'_iff]
  rfl

Goal state after:
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 ε : ℝ
x y : M ⧸ S
⊢ infDist 1 {m | ↑m = x * y} ≤ infDist 1 {m | ↑m = x} + infDist 1 {m | ↑m = y}

Tactic:
by
    simp only [infDist_eq_iInf]
    have := (norm_aux x).to_subtype
    have := (norm_aux y).to_subtype
    refine le_ciInf_add_ciInf ?_
    rintro ⟨a, rfl⟩ ⟨b, rfl⟩
    refine ciInf_le_of_le ⟨0, forall_mem_range.2 fun _ ↦ dist_nonneg⟩ ⟨a * b, rfl⟩ ?_
    simpa using norm_mul_le' _ _

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

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

Tactic:
exact sin_eq_zero_iff

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
x y : Set E
⊢ ↑1 * ediam x + ↑1 * ediam y = ediam x + ediam y

Tactic:
simp only [ENNReal.coe_one, one_mul]

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

Goal state before:
pp: n : ℤ
hx₁ : -(2 * π) < ↑n * (2 * π)
hx₂ : ↑n * (2 * π) < 2 * π
h : cos (↑n * (2 * π)) = 1
⊢ ↑n * (2 * π) = 0

Tactic:
rw [mul_lt_iff_lt_one_left two_pi_pos] at hx₂

Goal state after:
n : ℤ
hx₁ : -(2 * π) < ↑n * (2 * π)
hx₂ : ↑n < 1
h : cos (↑n * (2 * π)) = 1
⊢ ↑n * (2 * π) = 0
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:
mul_one

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

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

Tactic:
by subst_vars; rfl

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

Goal state before:
pp: case e'_3.f
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ s
x : E
⊢ x ∈ ball x✝¹ δ ↔ x ∈ ball (x✝¹ * 1) δ

Tactic:
mul_one

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
⊢ ball 0 (‖c‖ * 1) = ball 0 ‖c‖

Tactic:
mul_one

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
⊢ ball 0 ‖c‖ = ball 0 ‖c‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ (4 • X ^ 2 - 2 • X - C 1).IsRoot (cos (π / 5))

Tactic:
by
  simpa using quadratic_root_cos_pi_div_five

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

Goal state before:
pp: case inr
c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / (2 * 4)
⊢ c = (1 + √5) / 4

Tactic:
· absurd (show 0 ≤ c from cos_nonneg_of_mem_Icc <| by constructor <;> linarith [pi_pos.le])
    rw [not_le, h]
    exact div_neg_of_neg_of_pos (by norm_num [lt_sqrt]) (by positivity)

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

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
⊢ infEDist x (thickening δ s) = infEDist x s - ENNReal.ofReal δ

Tactic:
refine (tsub_le_iff_right.2 infEDist_le_infEDist_thickening_add).antisymm' ?_

Goal state after:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
⊢ infEDist x (thickening δ s) ≤ infEDist x s - ENNReal.ofReal δ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ Tendsto cos (𝓝[>] (-(π / 2))) (𝓝[>] 0)

Tactic:
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
  · convert! continuous_cos.continuousWithinAt.tendsto
    simp
  · filter_upwards [Ioo_mem_nhdsGT (neg_lt_self pi_div_two_pos)] with x hx
    exact cos_pos_of_mem_Ioo hx

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

Goal state before:
pp: ⊢ Function.Periodic cosh (2 * ↑π * I)

Tactic:
convert! cosh_antiperiodic.periodic_two_mul using 1
  ring

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
⊢ closedBall 0 (‖c‖ * 1) = closedBall 0 ‖c‖

Tactic:
mul_one

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
⊢ closedBall 0 ‖c‖ = closedBall 0 ‖c‖
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: 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
⊢ (𝓝 (const X c)).HasBasis (fun Ki ↦ IsCompact Ki.1 ∧ p Ki.2) fun Ki ↦ {f | MapsTo (⇑f) Ki.1 (U Ki.2)}

Tactic:
refine ⟨fun s ↦ ⟨fun hs ↦ ?_, fun hs ↦ ?_⟩⟩
  · rcases ContinuousMap.mem_nhds_iff.mp hs with ⟨S, hSf, hS, hSsub⟩
    choose hScompact hSopen hSmaps using hS
    have : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c := by
      simp only [biInter_mem hSf, Prod.forall, iInter_mem]
      rintro K U hKU ⟨x, hx⟩
      exact (hSopen K U hKU).mem_nhds <| hSmaps K U hKU hx
    rcases h.mem_iff.mp this with ⟨i, hpi, hi⟩
    refine ⟨(⋃ KU ∈ S, KU.1, i), ⟨hSf.isCompact_biUnion <| Prod.forall.2 hScompact, hpi⟩,
      Subset.trans ?_ hSsub⟩
    intro f hf K V hKV
    rcases K.eq_empty_or_nonempty with rfl | hKne
    · exact mapsTo_empty _ _
    · refine hf.out.mono (subset_biUnion_of_mem (u := Prod.fst) hKV) (hi.trans ?_)
      exact (biInter_subset_of_mem hKV).trans <| iInter_subset _ hKne
  · rcases hs with ⟨⟨K, i⟩, ⟨hK, hpi⟩, hi⟩
    filter_upwards [eventually_mapsTo hK isOpen_interior fun x _ ↦
      mem_interior_iff_mem_nhds.mpr <| h.mem_of_mem hpi] with f hf
    exact hi <| hf.mono_right interior_subset

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

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

Tactic:
simp only [snoc_zero]

Goal state after:
case snoc.elim0
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
s : Set X
h : IsPathConnected s
x : X
hp : ∀ (i : Fin 0), i.elim0 ∈ s
hx : x ∈ s
⊢ ∃ γ, range ⇑γ ⊆ s ∧ ∀ (i : Fin 0), i.elim0 ∈ range ⇑γ
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
T : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace T
f : T → X → Y
g : C(X, Y)
f_cont : Continuous[instTopologicalSpaceProd, inst✝¹] (Function.uncurry f)
this : ∀ (x : T), Continuous[inst✝², inst✝¹] (f x)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] (Function.uncurry fun x y ↦ (mkD (f x) g) y)

Tactic:
conv in mkD _ _ => rw [mkD_of_continuous (this x)]

Goal state after:
X : Type u_2
Y : Type u_3
T : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace T
f : T → X → Y
g : C(X, Y)
f_cont : Continuous[instTopologicalSpaceProd, inst✝¹] (Function.uncurry f)
this : ∀ (x : T), Continuous[inst✝², inst✝¹] (f x)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] (Function.uncurry fun x y ↦ { toFun := f x, continuous_toFun := ⋯ } y)
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : IsPathConnected s
ht : IsPathConnected t
⊢ IsPathConnected (s ×ˢ t)

Tactic:
by
  rw [isPathConnected_iff]
  refine ⟨hs.nonempty.prod ht.nonempty, fun (x₁, y₁) ⟨hx₁, hy₁⟩ (x₂, y₂) ⟨hx₂, hy₂⟩ ↦ ?_⟩
  exact hs.joinedIn x₁ hx₁ x₂ hx₂ |>.prod <| ht.joinedIn y₁ hy₁ y₂ hy₂

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 : Y × X → Z
hg : Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ g (p.1, f p.2)
this✝ : Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ g (p.swap.1, f p.swap.2)
this : Continuous[instTopologicalSpaceProd, inst✝¹] fun p ↦ (g ∘ Prod.swap) (f p.1, p.2)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] g

Tactic:
exact (hf.continuous_lift_prod_left this).comp continuous_swap

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

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

Tactic:
mul_one

Goal state after:
case inr.left
p✝ x : ℝ
hp✝ : p✝ ≠ 0
p : ℝ
hp : 0 < p
hx : |x| ≤ p / 2
hx' : x ≠ p / 2
hx₁ : -(p / 2) ≤ x
hx₂ : x < p / 2
⊢ -(p / 2) ≤ x
Module: Mathlib.Topology.Path

Goal state before:
pp: case pos
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
x y z : X✝
ι : Type u_3
γ✝ : Path x y
X : Type u_4
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
h₁ : t₀ ≤ ↑0
h₂ : ↑0 ≤ t₁
h₃ : t₀ ≤ t₁
⊢ γ.extend ↑0 = γ.extend t₀

Tactic:
simp [γ.extend_of_le_zero h₁]

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
⊢ x < p * 1 / 2

Tactic:
mul_one

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

Goal state before:
pp: case inl.inl
x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|0| / 2)
hε : 0 ≤ ε
⊢ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < |0| / 2 then closedBall x ε ∩ s else s

Tactic:
simp only [not_lt.mpr hε, coe_real_preimage_closedBall_period_zero, abs_zero, zero_div,
        if_false, inter_eq_right]

Goal state after:
case inl.inl
x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|0| / 2)
hε : 0 ≤ ε
⊢ s ⊆ closedBall x ε
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr.inr.inr.inr
p x ε : ℝ
s : Set ℝ
hε : ε < |p| / 2
z : ℤ
hs : s ⊆ Icc (x - |p| / 2) (x + |p| / 2)
hz : z ≠ 0
y : ℝ
hy₀ : y ∈ s
hy₁ : x + ↑z * p - ε ≤ y
hy₂ : y ≤ x + ↑z * p + ε
hy₃ : x - |p| / 2 ≤ y
hy₄ : y ≤ x + |p| / 2
hp : p < 0
⊢ False

Tactic:
rcases Int.cast_le_neg_one_or_one_le_cast_of_ne_zero ℝ hz with hz' | hz'
      · have : -p ≤ ↑z * p := by nlinarith
        linarith [abs_eq_neg_self.mpr hp.le]
      · have : ↑z * p ≤ p := by nlinarith
        linarith [abs_eq_neg_self.mpr hp.le]

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

Goal state before:
pp: case inr.inr.refine_2
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ -arcsin x ∈ Icc (-(π / 2)) (π / 2)

Tactic:
· exact ⟨neg_le_neg (arcsin_le_pi_div_two _), neg_le.2 (neg_pi_div_two_le_arcsin _)⟩

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

Goal state before:
pp: α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
ε : ℝ
hε0 : 0 < ε
⊢ ∀ᶠ (x : α) in l, g x ∈ closedBall 0 ε

Tactic:
filter_upwards [hc, hasBasis_cobounded_norm.tendsto_right_iff.mp hf (c / ε) trivial,
    hf.eventually_ne_cobounded 0] with x hfgc hεf hf0

Goal state after:
α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
ε : ℝ
hε0 : 0 < ε
x : α
hfgc : ‖f x • g x‖ ≤ c
hεf : c / ε ≤ ‖f x‖
hf0 : f x ≠ 0
⊢ g x ∈ closedBall 0 ε
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg.mpr
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : 0 < y
⊢ { re := 0, im := y }.arg = { re := 0, im := y * 1 }.arg

Tactic:
mul_one

Goal state after:
case neg.mpr
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : 0 < y
⊢ { re := 0, im := y }.arg = { re := 0, im := y }.arg
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x : ℂ
⊢ (log x).re = Real.log ‖x‖

Tactic:
simp [log]

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

Goal state before:
pp: x : ℂ
⊢ (log x).im = x.arg

Tactic:
simp [log]

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

Goal state before:
pp: ⊢ log 0 = 0

Tactic:
simp [log]

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

Goal state before:
pp: ⊢ log 1 = 0

Tactic:
simp [log]

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

Goal state before:
pp: x : ℂ
⊢ log (x / x) = 0

Tactic:
simp [log]

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

Goal state before:
pp: ⊢ log (-1) = ↑π * I

Tactic:
simp [log]

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

Goal state before:
pp: ⊢ log I = ↑π / 2 * I

Tactic:
simp [log]

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

Goal state before:
pp: ⊢ log (-I) = -(↑π / 2) * I

Tactic:
simp [log]

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

Goal state before:
pp: ⊢ 2 * π = 2 * π * 1

Tactic:
mul_one

Goal state after:
⊢ 2 * π = 2 * π
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: case pos
s : Set ℂ
hs : s.Countable
z : ℂ
hz : z ∈ s
h : ∃ w, cexp w = z
⊢ (cexp ⁻¹' {z}).Countable

pp: case neg
s : Set ℂ
hs : s.Countable
z : ℂ
hz : z ∈ s
h : ∀ (w : ℂ), cexp w ≠ z
⊢ (cexp ⁻¹' {z}).Countable

Tactic:
· rcases h with ⟨w, rfl⟩
      simp only [Set.preimage, Set.mem_singleton_iff, exp_eq_exp_iff_exists_int, Set.ofPred_exists]
      exact Set.countable_iUnion fun m => Set.countable_singleton _

Goal state after:
case neg
s : Set ℂ
hs : s.Countable
z : ℂ
hz : z ∈ s
h : ∀ (w : ℂ), cexp w ≠ z
⊢ (cexp ⁻¹' {z}).Countable
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: n m : ℕ
z : ℂ
⊢ ↑n ^ (↑m * z) = (↑n ^ m) ^ z

Tactic:
refine cpow_nat_mul' (x := n) (n := m) ?_ ?_ z
  · simp only [natCast_arg, mul_zero, Left.neg_neg_iff, pi_pos]
  · simp only [natCast_arg, mul_zero, pi_pos.le]

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

Goal state before:
pp: case h
ψ x✝ : ℝ
⊢ (↑x✝).sin = Real.sin ψ ↔ ↑x✝ = ↑ψ ∨ ↑x✝ + ↑ψ = ↑π

Tactic:
exact sin_eq_iff_coe_eq_or_add_eq_pi

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

Goal state before:
pp: x : ℂ
⊢ ↑((starRingEnd ℂ) x).arg = -↑x.arg

Tactic:
by
  by_cases h : arg x = π <;> simp [arg_conj, h]

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

Goal state before:
pp: x : ℂ
⊢ ↑x⁻¹.arg = -↑x.arg

Tactic:
by
  by_cases h : arg x = π <;> simp [arg_inv, h]

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

Goal state before:
pp: case neg
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : ¬θ = π
⊢ |θ| = θ

Tactic:
abs_eq_self.2 h.1

Goal state after:
case neg
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : ¬θ = π
⊢ θ = θ
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: x : ℂ
hx_re : x.re < 0
hx_im : x.im < 0
⊢ arg =ᶠ[𝓝 x] fun x ↦ Real.arcsin ((-x).im / ‖x‖) - π

Tactic:
suffices h_forall_nhds : ∀ᶠ y : ℂ in 𝓝 x, y.re < 0 ∧ y.im < 0 from
    h_forall_nhds.mono fun y hy => arg_of_re_neg_of_im_neg hy.1 hy.2
  refine IsOpen.eventually_mem ?_ (⟨hx_re, hx_im⟩ : x.re < 0 ∧ x.im < 0)
  exact
    IsOpen.and (isOpen_lt continuous_re continuous_zero) (isOpen_lt continuous_im continuous_zero)

Goal state after: