mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
⊢ map Prod.swap (μ.prod ν) = ν.prod μ

Tactic:
have : sum (fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)))
       = sum (fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))) := by
    ext s hs
    rw [sum_apply _ hs, sum_apply _ hs]
    exact ((Equiv.prodComm ℕ ℕ).tsum_eq _).symm

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
this :
  (sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) =
    sum fun i ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))
⊢ map Prod.swap (μ.prod ν) = ν.prod μ
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α✝ : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β✝ : Type u_5
inst✝⁴ : MeasurableSpace β✝
β : Type u_6
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : StandardBorelSpace α
inst✝ : StandardBorelSpace β
h : ¬Countable α
this : UpgradedStandardBorel α := upgradeStandardBorel α
f : (ℕ → Bool) → α
fcts : Continuous[_, this.toTopologicalSpace] f
finj : Injective f
g : α → ℕ → Bool
gmeas : Measurable g
ginj : Injective g
⊢ Nonempty (α ≃ᵐ (ℕ → Bool))

Tactic:
exact ⟨borelSchroederBernstein gmeas ginj fcts.measurable finj⟩

Goal state after:
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hμs : μ s = 0
hf : Measurable fun z ↦ (z.2 * z.1, z.1⁻¹)
this : (map (fun z ↦ (z.2 * z.1, z.1⁻¹)) (μ.prod μ)) (s⁻¹ ×ˢ s⁻¹) = 0
⊢ μ s⁻¹ = 0

Tactic:
simpa only [(measurePreserving_mul_prod_inv μ μ).map_eq, prod_prod, mul_eq_zero (M₀ := ℝ≥0∞),
      or_self_iff] using this

Goal state after:
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hμs : μ s = 0
hf : Measurable fun z ↦ (z.2 * z.1, z.1⁻¹)
hsm' : MeasurableSet (s⁻¹ ×ˢ s⁻¹)
⊢ (map (fun z ↦ (z.2 * z.1, z.1⁻¹)) (μ.prod μ)) (s⁻¹ ×ˢ s⁻¹) = 0

Tactic:
map_apply hf hsm',

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hμs : μ s = 0
hf : Measurable fun z ↦ (z.2 * z.1, z.1⁻¹)
hsm' : MeasurableSet (s⁻¹ ×ˢ s⁻¹)
⊢ (μ.prod μ) ((fun z ↦ (z.2 * z.1, z.1⁻¹)) ⁻¹' s⁻¹ ×ˢ s⁻¹) = 0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : (μ.withDensity f) s = 0
t : Set α := toMeasurable (μ.withDensity f) s
A : μ {a | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0)} = 0
x : α
⊢ x ∈ {x | f x ≠ 0} ∩ toMeasurable (μ.withDensity f) s ↔ x ∈ {a | ¬(a ∈ toMeasurable (μ.withDensity f) s → f a = 0)}

Tactic:
simp only [and_comm, exists_prop, mem_inter_iff, mem_ofPred_eq,
      not_forall]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
U : Set α
hUo : IsOpen[inst✝⁴] U
hμU : μ U < ∞
hUs : μ (U ∆ t) < ε
⊢ μ (U ∆ s) < ε

Tactic:
measure_congr <| (ae_eq_refl _).symmDiff hst

Goal state after:
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
t : Set α
htm : MeasurableSet t
hst : s =ᵐ[μ] t
U : Set α
hUo : IsOpen[inst✝⁴] U
hμU : μ U < ∞
hUs : μ (U ∆ t) < ε
⊢ μ (U ∆ t) < ε
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: ⊢ Continuous fun x ↦ √x

Tactic:
unfold sqrt; fun_prop

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 : Set α
left✝ : t ⊆ univ
ht : MeasurableSet t
htendsto : μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop (univ \ t)
⊢ μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop tᶜ

Tactic:
Set.compl_eq_univ_sdiff

Goal state after:
α : 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 : Set α
left✝ : t ⊆ univ
ht : MeasurableSet t
htendsto : μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop (univ \ t)
⊢ μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop (univ \ t)
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
h : √x < y
hy : 0 < y
⊢ x < y ^ 2

Tactic:
← sqrt_lt_sqrt_iff_of_pos (sq_pos_of_pos hy),

Goal state after:
x y : ℝ
h : √x < y
hy : 0 < y
⊢ √x < √(y ^ 2)
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ √(x ^ 2 + y ^ 2) ≤ √(m ^ 2 + m ^ 2)

Tactic:
gcongr √(?_ + ?_)

Goal state after:
case h₁
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ x ^ 2 ≤ m ^ 2

case h₂
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ y ^ 2 ≤ m ^ 2
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:

Tactic:
∫⁻ a, g a ∂μ.withDensity f = ∫⁻ a, g a ∂μ.withDensity f' := by
      rw [withDensity_congr_ae hf.ae_eq_mk]
    _ = ∫⁻ a, (f' * g) a ∂μ := by
      apply lintegral_withDensity_eq_lintegral_mul_non_measurable _ hf.measurable_mk
      filter_upwards [h'f, hf.ae_eq_mk]
      intro x hx h'x
      rwa [← h'x]
    _ = ∫⁻ a, (f * g) a ∂μ := by
      apply lintegral_congr_ae
      filter_upwards [hf.ae_eq_mk]
      intro x hx
      simp only [f', hx, Pi.mul_apply]

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U : R
hU : U ∈ unitary R
⊢ star U * star (star U) = 1

Tactic:
by rw [star_star, star_mul_self_of_mem hU]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Ring 𝕜₂
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : 𝕜 →ₗ[𝕜] E
x : 𝕜
⊢ ‖x • f 1‖ ≤ ‖x‖ * ‖f 1‖

Tactic:
exact norm_smul_le _ _

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

Goal state before:
pp: case pos
ι : 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 ι
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : Summable f L
hL : L.NeBot
⊢ ∑'[L] (z : ι), e (f z) = y ↔ ∑'[L] (z : ι), f z = e.symm y

Tactic:
exact ⟨fun h ↦ (e.hasSum.mp ((e.summable.mpr hf).hasSum_iff.mpr h)).tsum_eq, fun h ↦
        (e.hasSum.mpr (hf.hasSum_iff.mpr h)).tsum_eq⟩

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

Goal state before:
pp: ⊢ Metric.ball 1 1 ⊆ slitPlane

Tactic:
intro z

Goal state after:
z : ℂ
⊢ z ∈ Metric.ball 1 1 → z ∈ slitPlane
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
z w : ℝ
⊢ (AddMonoidHom.id ℝ) (z * w) = (AddMonoidHom.id ℝ) z * (AddMonoidHom.id ℝ) w - 0 z * 0 w

Tactic:
by simp only [sub_zero, mul_zero, AddMonoidHom.zero_apply, AddMonoidHom.id_apply]

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ IsOpen[inst✝] (↑e '' e.source)

Tactic:
image_source_eq_target

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ IsOpen[inst✝] e.target
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
p : X → Prop
s : Set X
hx : x ∈ e.source
⊢ (∀ᶠ (y : Y) in 𝓝[↑e.symm ⁻¹' s] ↑e x, p (↑e.symm y)) ↔ ∀ᶠ (x : X) in 𝓝[s] x, p x

Tactic:
by
  rw [e.eventually_nhdsWithin _ hx]
  refine eventually_congr <|
    (eventually_nhdsWithin_of_eventually_nhds <| e.eventually_left_inverse hx).mono fun y hy => ?_
  rw [hy]

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
f : α → E
g'' : α → F''
l : Filter α
h : ∀ᶠ (x : α) in l, g'' x ≠ 0
⊢ f =O[l] g'' ↔ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f x‖ / ‖g'' x‖

Tactic:
simp only [isBigO_iff, IsBoundedUnder, IsBounded, eventually_map]
  exact
    exists_congr fun c =>
      eventually_congr <| h.mono fun x hx => (div_le_iff₀ <| norm_pos_iff.2 hx).symm

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 g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
⊢ ∃ i,
    ∀ j ≥ i, abv ((∑ k ∈ range j, f k) * ∑ k ∈ range j, g k - ∑ n ∈ range j, ∑ m ∈ range (n + 1), f m * g (n - m)) < ε

Tactic:
have hQε0 : 0 < ε / (4 * Q) :=
    div_pos ε0 (mul_pos (show (0 : α) < 4 by simp) (lt_of_le_of_lt (abv_nonneg _ _) (hQ 0)))

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
⊢ ∃ i,
    ∀ j ≥ i, abv ((∑ k ∈ range j, f k) * ∑ k ∈ range j, g k - ∑ n ∈ range j, ∑ m ∈ range (n + 1), f m * g (n - m)) < ε
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: ⊢ rexp 0 = 1

Tactic:
simp [Real.exp]

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

Goal state before:
pp: x : ℂ
h1 : x + 2 * x = 3 * x
⊢ sinh (3 * x) = 4 * sinh x ^ 3 + 3 * sinh x

Tactic:
rw [← h1, sinh_add x (2 * x)]

Goal state after:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ sinh x * cosh (2 * x) + cosh x * sinh (2 * x) = 4 * sinh x ^ 3 + 3 * sinh x
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
h : I * sin (x * I) = -sinh x
⊢ sin (x * I) = - -sinh x * I

Tactic:
← h

Goal state after:
x : ℂ
h : I * sin (x * I) = -sinh x
⊢ sin (x * I) = -(I * sin (x * I)) * I
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case pos
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
x : α
hx : C⁻¹ ≤ ‖g x‖ / ‖f x‖
hf : f x = 0
⊢ ‖f x‖ ≤ C * ‖g x‖

Tactic:
simp [hf] at hx
    linarith

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

Goal state before:
pp: case hab
x✝ : ℂ
hx : ‖x✝‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
x : ℕ
a✝ : x ∈ {m ∈ range j | n ≤ m}
⊢ ‖x✝‖ ^ (x - n) ≤ 1

Tactic:
exact pow_le_one₀ (norm_nonneg _) hx

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

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

Tactic:
by
  refine ⟨lt_imp_lt_of_le_imp_le (zpow_nonneg · _), fun ha ↦ ?_⟩
  obtain ⟨k, rfl⟩ := hn
  rw [zpow_add_one₀ ha.ne]
  exact mul_neg_of_pos_of_neg (Even.zpow_pos (even_two_mul _) ha.ne) ha

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

Goal state before:
pp: r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
⊢ ∀ (z : ℂ), ‖z‖ ≤ 1 → ‖cexp (x + z) - cexp x‖ ≤ ‖z‖ * ‖cexp x‖ + ‖cexp x‖ * ‖z‖ ^ 2

Tactic:
intro z

Goal state after:
r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
z : ℂ
⊢ ‖z‖ ≤ 1 → ‖cexp (x + z) - cexp x‖ ≤ ‖z‖ * ‖cexp x‖ + ‖cexp x‖ * ‖z‖ ^ 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:
Int.cast_add,

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
inst✝ : SeminormedCommGroup M
S : Subgroup M
m : M
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑S
⊢ ‖↑m‖ = 0 ↔ m ∈ S

Tactic:
by
  rw [norm_mk_eq_zero_iff_mem_closure, hS.closure_eq, SetLike.mem_coe]

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

Goal state before:
pp: case inr.inr
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
⊢ y ∈ ball x (dist y x)

Tactic:
suffices f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1 by
    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:
case inr.inr
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
⊢ f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: case cons
M : Type u_4
inst✝² : MulOneClass M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l l' : List M
a✝¹ b✝ : M
l₁✝ l₂✝ : List M
h₁ : Joined a✝¹ b✝
a✝ : List.Forall₂ Joined l₁✝ l₂✝
h₂ : Joined l₁✝.prod l₂✝.prod
⊢ Joined (a✝¹ :: l₁✝).prod (b✝ :: l₂✝).prod

Tactic:
exact h₁.mul h₂

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

Goal state before:
pp: case right
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn F x = F
y : X
y_in : y ∈ F
⊢ JoinedIn F x y

Tactic:
← h

Goal state after:
case right
X : Type u_1
inst✝ : TopologicalSpace X
F : Set X
x : X
x_in : x ∈ F
h : pathComponentIn F x = F
y : X
y_in : y ∈ pathComponentIn F x
⊢ JoinedIn F x y
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ compactOpen = ⨅ K, ⨅ (_ : IsCompact K), induced (restrict K) compactOpen

Tactic:
by
  refine le_antisymm (le_iInf₂ fun s _ ↦ compactOpen_le_induced s) ?_
  refine le_generateFrom <| forall_mem_image2.2 fun K (hK : IsCompact K) U hU ↦ ?_
  refine TopologicalSpace.le_def.1 (iInf₂_le K hK) _ ?_
  convert! isOpen_induced (isOpen_setOfPred_mapsTo (isCompact_iff_isCompact_univ.1 hK) hU)
  simp [Subtype.forall, MapsTo]

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

Goal state before:
pp: α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
a✝ : ℕ
hn : 1 ≤ ‖f (a✝ + 1)‖ / 0
hc : ‖f a✝‖ = 0
⊢ False

Tactic:
_root_.div_zero

Goal state after:
α : Type u_4
inst✝ : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
a✝ : ℕ
hn : 1 ≤ 0
hc : ‖f a✝‖ = 0
⊢ False
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ✝ : Path x y
a b : X
γ : Path a b
⊢ γ.extend 1 = b

Tactic:
γ.extend_one

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ✝ : Path x y
a b : X
γ : Path a b
⊢ b = b
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : ε < |p| / 2
⊢ ∀ (z : ℤ), closedBall (x + z • p) ε ∩ s = if z = 0 then closedBall x ε ∩ s else ∅

Tactic:
intro z

Goal state after:
case inr
p x ε : ℝ
s : Set ℝ
hs : s ⊆ closedBall x (|p| / 2)
hε : ε < |p| / 2
z : ℤ
⊢ closedBall (x + z • p) ε ∩ s = if z = 0 then closedBall x ε ∩ s else ∅
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: z : ℂ
⊢ z.arg < π ↔ 0 ≤ z.re ∨ z.im ≠ 0

Tactic:
rw [(arg_le_pi z).lt_iff_ne, not_iff_comm, not_or, not_le, Classical.not_not, arg_eq_pi_iff]

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

Goal state before:
pp: x : ℂ
hx : x ≠ 0
⊢ cexp (↑(Real.log ‖x‖) + ↑x.arg * I) = x

Tactic:
exp_add_mul_I,

Goal state after:
x : ℂ
hx : x ≠ 0
⊢ cexp ↑(Real.log ‖x‖) * (cos ↑x.arg + sin ↑x.arg * I) = x
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case negSucc
x : ℝ
a✝ : ℕ
⊢ log (x ^ (a✝ + 1))⁻¹ = ↑(Int.negSucc a✝) * log x

Tactic:
log_inv,

Goal state after:
case negSucc
x : ℝ
a✝ : ℕ
⊢ -log (x ^ (a✝ + 1)) = ↑(Int.negSucc a✝) * log x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Log

Goal state before:
pp: x y : ℂ
⊢ cexp x = cexp y ↔ cexp (x - y) = 1

Tactic:
rw [exp_sub, div_eq_one_iff_eq (exp_ne_zero _)]

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

Goal state before:
pp: s : Set ℂ
⊢ (cexp ⁻¹' s).Countable ↔ s.Countable

Tactic:
refine ⟨fun hs => ?_, fun hs => ?_⟩
  · refine ((hs.image exp).insert 0).mono ?_
    rw [Set.image_preimage_eq_inter_range, range_exp, ← Set.sdiff_eq, ← Set.union_singleton,
        Set.sdiff_union_self]
    exact Set.subset_union_left
  · rw [← Set.biUnion_preimage_singleton]
    refine hs.biUnion fun z hz => ?_
    by_cases! h : ∃ w, exp w = z
    · 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 _
    · simp [Set.preimage, h]

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

Goal state before:
pp: case pos
x : ℂ
h✝¹ : 1 = 0
h✝ : x = 0
⊢ 1 = 1

Tactic:
simp_all [one_ne_zero]

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

Goal state before:
pp: case neg
x : ℂ
h✝¹ : 1 = 0
h✝ : ¬x = 0
⊢ 0 = 1

Tactic:
simp_all [one_ne_zero]

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

Goal state before:
pp: case neg
x : ℂ
h✝ : ¬1 = 0
⊢ cexp (log 1 * x) = 1

Tactic:
simp_all [one_ne_zero]

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

Goal state before:
pp: case mpr.inr
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * ↑k
⊢ -2 * sin ((θ + ψ) / 2) * sin ((θ - ψ) / 2) = 0

Tactic:
← sub_neg_eq_add,

Goal state after:
case mpr.inr
θ ψ : ℝ
k : ℤ
H : θ - -ψ = 2 * π * ↑k
⊢ -2 * sin ((θ - -ψ) / 2) * sin ((θ - ψ) / 2) = 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Complex

Goal state before:
pp: x : ℂ
n : ℤ
hlt : -π < ↑n * x.arg
hle : ↑n * x.arg ≤ π
y : ℂ
⊢ x ^ (↑n * y) = (x ^ n) ^ y

Tactic:
rw [mul_comm] at hlt hle

Goal state after:
x : ℂ
n : ℤ
hlt : -π < x.arg * ↑n
hle : x.arg * ↑n ≤ π
y : ℂ
⊢ x ^ (↑n * y) = (x ^ n) ^ y
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ Real.arcsin ((-z).im / ‖z‖) - π < -(π / 2)

Tactic:
sub_lt_iff_lt_add',

Goal state after:
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ Real.arcsin ((-z).im / ‖z‖) < π + -(π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ ψ : ℝ
⊢ toIocMod two_pi_pos ψ θ - θ = 2 * π * ↑(-toIocDiv two_pi_pos ψ θ)

Tactic:
toIocMod_sub_self,

Goal state after:
θ ψ : ℝ
⊢ -toIocDiv two_pi_pos ψ θ • (2 * π) = 2 * π * ↑(-toIocDiv two_pi_pos ψ θ)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case pos
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : θ = π
⊢ |(-↑θ).toReal| = θ

Tactic:
simp [hnegpi, Real.pi_pos.le]

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

Goal state before:
pp: r : ℝ
hr : 0 < r
θ : ℝ
⊢ toIocMod Real.two_pi_pos (-π) θ - θ = 2 * π * ↑⌊(π - θ) / (2 * π)⌋

Tactic:
toIocMod_sub_self,

Goal state after:
r : ℝ
hr : 0 < r
θ : ℝ
⊢ -toIocDiv Real.two_pi_pos (-π) θ • (2 * π) = 2 * π * ↑⌊(π - θ) / (2 * π)⌋
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr.inr
w : ℂ
h : 0 = 0 → w.re = 0 → w = 0
hw : w.re ≠ 0
⊢ w ≠ 0

Tactic:
exact ne_of_apply_ne re hw

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: a b : ℝ
h : a ≠ 0
⊢ ContinuousAt (fun x ↦ a ^ x) b

Tactic:
simp only [rpow_def]

Goal state after:
a b : ℝ
h : a ≠ 0
⊢ ContinuousAt (fun x ↦ (↑a ^ ↑x).re) b
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: a b : ℝ
h : b ≠ 0
⊢ ContinuousAt (fun x ↦ a ^ x) b

Tactic:
simp only [rpow_def]

Goal state after:
a b : ℝ
h : b ≠ 0
⊢ ContinuousAt (fun x ↦ (↑a ^ ↑x).re) b
Module: Mathlib.Analysis.SpecialFunctions.Pow.Continuity

Goal state before:
pp: x : ℝ
y : ℂ
h : 0 < y.re ∨ x ≠ 0
hx : x < 0
this : ContinuousAt (fun p ↦ (-↑p.1) ^ p.2 * cexp (↑π * I * p.2)) (x, y)
⊢ ∀ x ∈ Set.Iio 0 ×ˢ Set.univ, (fun p ↦ (-↑p.1) ^ p.2 * cexp (↑π * I * p.2)) x = (fun p ↦ ↑p.1 ^ p.2) x

Tactic:
exact fun p hp => (ofReal_cpow_of_nonpos (le_of_lt hp.1) p.2).symm

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: case neg
y : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ (-y) = (↑x ^ y)⁻¹

Tactic:
have A : x ^ y ≠ 0 := by simp [h]
      simp [← coe_rpow_of_ne_zero h, ← coe_inv A, NNReal.rpow_neg]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NNReal

Goal state before:
pp: x : ℝ≥0∞
n : ℕ
⊢ x ^ ↑n = x ^ n

Tactic:
by
  cases x
  · cases n <;> simp [top_rpow_of_pos (Nat.cast_add_one_pos _), top_pow (Nat.succ_ne_zero _)]
  · simp [← coe_rpow_of_nonneg _ (Nat.cast_nonneg n)]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: x : ℝ
hx : x ≠ 0
y : ℝ
hy : y ∈ {y | 0 ≤ y}
z : ℝ
hz : z ∈ {y | 0 ≤ y}
hyz : y ^ x = z ^ x
⊢ (y ^ x) ^ x⁻¹ = z ^ (x * x⁻¹)

Tactic:
rpow_mul hz,

Goal state after:
x : ℝ
hx : x ≠ 0
y : ℝ
hy : y ∈ {y | 0 ≤ y}
z : ℝ
hz : z ∈ {y | 0 ≤ y}
hyz : y ^ x = z ^ x
⊢ (y ^ x) ^ x⁻¹ = (z ^ x) ^ x⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case inr
n : ℕ
ε : ℝ
hε : 0 < ε
h : n > 0
⊢ ‖log ↑n‖ ≤ ↑n ^ ε / ε

Tactic:
← natCast_log,

Goal state after:
case inr
n : ℕ
ε : ℝ
hε : 0 < ε
h : n > 0
⊢ ‖↑(Real.log ↑n)‖ ≤ ↑n ^ ε / ε