mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C✝ : ℝ
f : ℂ → E
z : ℂ
C : ℝ
hC₀ : 0 < C
a b : ℝ
hza : a - b < z.im
hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C
hzb : z.im < a + b
hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C
hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))
hab : a - b < a + b
hb : 0 < b
hπb : 0 < π / 2 / b
c : ℝ
hc : c < π / 2 / b
B : ℝ
hO : f =O[comap (abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z ↦ expR (B * expR (c * |z.re|))
d : ℝ
hd : d < π / 2 / b
hcd : c < d
hd₀ : 0 < d
hb' : d * b < π / 2
aff : ℂ → ℂ := fun w ↦ ↑d * (w - ↑a * I)
g : ℝ → ℂ → ℂ := fun ε w ↦ cexp (↑ε * (cexp (aff w) + cexp (-aff w)))
ε : ℝ
ε₀ : ε < 0
δ : ℝ
δ₀ : δ < 0
hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → ‖g ε w‖ ≤ expR (δ * expR (d * |w.re|))
hg₁ : ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → ‖g ε w‖ ≤ 1
A : ℝ
hA₀ : A > 0
hA :
  ∀ᶠ (b_1 : ℝ) in atTop,
    ∀ (a_1 : ℂ), |a_1.re| = b_1 → a - b < a_1.im ∧ a_1.im < a + b → ‖f a_1‖ ≤ A * expR (B * expR (c * |a_1.re|))
this : Tendsto (fun R ↦ expR (δ * expR (d * R) + B * expR (c * R) + Real.log A)) atTop (𝓝 0)
⊢ ∀ᶠ (R : ℝ) in atTop, ∀ (w : ℂ), |w.re| = R → w.im ∈ Ioo (a - b) (a + b) → ‖g ε w • f w‖ ≤ C

Tactic:
by
      filter_upwards [this.eventually (ge_mem_nhds hC₀), hA] with R hR Hle w hre him
      calc
        ‖g ε w • f w‖ ≤ expR (δ * expR (d * R) + B * expR (c * R) + Real.log A) := ?_
        _ ≤ C := hR
      rw [norm_smul, Real.exp_add, ← hre, Real.exp_add, Real.exp_log hA₀, mul_assoc, mul_comm _ A]
      gcongr
      exacts [hδ <| Ioo_subset_Icc_self him, Hle _ hre him]

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

Goal state before:
pp: case hf.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hz : z ∈ verticalStrip 0 1
this :
  ∀ x ∈ Ioi 0,
    (x + sSupNormIm f 0) ^ (1 - z.re) * (x + sSupNormIm f 1) ^ z.re =
      ‖↑(x + sSupNormIm f 0) ^ (1 - z) * ↑(x + sSupNormIm f 1) ^ z‖
⊢ Tendsto (fun a ↦ a + sSupNormIm f 0) (𝓝[>] 0) (𝓝 (0 + sSupNormIm f 0))

Tactic:
exact Tendsto.add_const (sSupNormIm f 0) (tendsto_nhdsWithin_of_tendsto_nhds
              (Continuous.tendsto continuous_id' _))

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

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
⊢ 0 ≤ sSupNormIm f 0 ^ (1 - z.re) ∧ 0 ≤ sSupNormIm f 1 ^ z.re

Tactic:
exact ⟨Real.rpow_nonneg (sSupNormIm_nonneg f _) _,
        Real.rpow_nonneg (sSupNormIm_nonneg f _) _ ⟩

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalAverage

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : b < a
⊢ (a - b)⁻¹ • ∫ (x : ℝ) in Ioc b a, f x = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x

Tactic:
integral_of_ge h.le,

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : b < a
⊢ (a - b)⁻¹ • ∫ (x : ℝ) in Ioc b a, f x = (b - a)⁻¹ • -∫ (x : ℝ) in Ioc b a, f x ∂volume
Module: Mathlib.MeasureTheory.Integral.CircleAverage

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℂ → E
c : ℂ
R : ℝ
⊢ circleAverage f c (-R) = circleAverage f c R

Tactic:
by
  unfold circleAverage
  simp_rw [circleMap_neg_radius, ← circleAverage_def, circleAverage_eq_integral_add π]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
this : Function.Periodic (fun x ↦ log ‖circleMap 0 1 x - 1‖) (2 * π)
⊢ ∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 (ζ + x) - 1‖ = ∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 x - 1‖

Tactic:
have := this.intervalIntegral_add_eq (t := 0) (s := ζ)

Goal state after:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
this✝ : Function.Periodic (fun x ↦ log ‖circleMap 0 1 x - 1‖) (2 * π)
this : ∫ (x : ℝ) in 0..0 + 2 * π, log ‖circleMap 0 1 x - 1‖ = ∫ (x : ℝ) in ζ..ζ + 2 * π, log ‖circleMap 0 1 x - 1‖
⊢ ∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 (ζ + x) - 1‖ = ∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 x - 1‖
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: w ρ : ℂ
R r : ℝ
hρ : ‖ρ‖ = R
hr_lt : r < R
hwr : ‖w‖ < r
⊢ Continuous fun θ ↦ herglotzLogIntegrand w ρ (circleMap 0 r θ)

Tactic:
rw [continuous_iff_continuousAt]
  intro θ
  apply ContinuousAt.comp (continuousAt_herglotzLogIntegrand _ _) (by fun_prop)
  all_goals
    by_contra h
    grind [norm_circleMap_zero, lt_of_le_of_lt (Complex.norm_nonneg w) hwr]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun z t ↦ z₀ + t • z
gray : E → ℂ → ℂ := fun z ↦ g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x | AnalyticAt ℂ g x}
z : E
hz : z ∈ sphere 0 1
t : ℂ
ht : t ∈ ball 0 r
⊢ ray z t ∈ ball z₀ r

Tactic:
simpa [ray, norm_smul, mem_sphere_zero_iff_norm.mp hz] using! ht

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

Goal state before:
pp: case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1) = 2 * ∏ i ∈ Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 3)
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * (k + 1) + 1) = (2 * ↑k + 2) / (2 * ↑k + 3) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)

Tactic:
mul_succ,

Goal state after:
case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1) = 2 * ∏ i ∈ Finset.range k, (2 * ↑i + 2) / (2 * ↑i + 3)
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 2 + 1) = (2 * ↑k + 2) / (2 * ↑k + 3) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) = π * ∏ i ∈ Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * (k + 1)) = (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k)

Tactic:
mul_succ,

Goal state after:
case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) = π * ∏ i ∈ Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)
⊢ ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 2) = (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k)
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ log ‖circleMap 0 r θ - ρ‖ ≤ |log (2 * R)| + 0 + 0

Tactic:
grw [← le_abs_self, norm_sub_le, hρ, two_mul, norm_circleMap_zero, abs_of_pos hr, hrR]

Goal state after:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ log (R + R) ≤ log (R + R) + 0 + 0
Module: Mathlib.Analysis.Complex.TaylorSeries

Goal state before:
pp: c : ℂ
r : ENNReal
z : ℂ
hz : z ∈ Metric.eball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.eball c r)
⊢ ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z

Tactic:
convert! taylorSeries_eq_on_eball hf hz using 3 with n

Goal state after:
case e'_5
c : ℂ
r : ENNReal
z : ℂ
hz : z ∈ Metric.eball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.eball c r)
n : ℕ
⊢ (↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c
Module: Mathlib.Analysis.Complex.RiemannMapping

Goal state before:
pp: case hf'
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
z : ℂ
hz : z ∈ U
⊢ 2 * f z ≠ 0

pp: case hfg
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
z : ℂ
hz : z ∈ U
⊢ ∀ᶠ (y : ℂ) in 𝓝 z, f y ^ 2 = y

Tactic:
· simpa using hf₀ z hz

Goal state after:
case hfg
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
z : ℂ
hz : z ∈ U
⊢ ∀ᶠ (y : ℂ) in 𝓝 z, f y ^ 2 = y
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hxc : x < c
⊢ f x ≤ f y

pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hcx : c ≤ x
⊢ f x ≤ f y

Tactic:
· have xs : x ∈ s := A _ hx hxc.le
    rcases lt_or_ge y c with (hyc | hcy)
    · exact h₁ xs (A _ hy hyc.le) hxy
    · exact (h₁ xs hs.1 hxc.le).trans (h₂ ht.1 (B _ hy hcy) hcy)

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hcx : c ≤ x
⊢ f x ≤ f y
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Disc

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
hn : Fintype.card n = 2
a✝ : Nontrivial R
⊢ A.charpoly.degree = 2

Tactic:
by simp; norm_cast

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
a b : R
⊢ { val := !![1, a + b; 0, 1], inv := !![1, -(a + b); 0, 1], val_inv := ⋯, inv_val := ⋯ } =
    { val := !![1, a; 0, 1], inv := !![1, -a; 0, 1], val_inv := ⋯, inv_val := ⋯ } *
      { val := !![1, b; 0, 1], inv := !![1, -b; 0, 1], val_inv := ⋯, inv_val := ⋯ }

Tactic:
simp [Units.ext_iff, add_comm]

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: ⊢ coe 1 = 1

Tactic:
by
  simp only [coe, map_one]

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: z : ℍ
⊢ denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) S)) ↑z = ↑z

Tactic:
simp [S, denom_apply]

Goal state after:
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((Matrix.comp m m n n R) (M.map ⇑f)).det * (f (M k k)).det ^ (Fintype.card m - 1) =
    ((Matrix.comp m m n n R) (M.map ⇑f)).det * ((Matrix.comp m m n n R) ((auxMat M k).map ⇑f)).det

Tactic:
((auxMat_blockTriangular M k).map f).comp.det_fintype,

Goal state after:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((Matrix.comp m m n n R) (M.map ⇑f)).det * (f (M k k)).det ^ (Fintype.card m - 1) =
    ((Matrix.comp m m n n R) (M.map ⇑f)).det *
      ∏ k_1, (((Matrix.comp m m n n R) ((auxMat M k).map ⇑f)).toSquareBlock (fun i ↦ i.1 ≠ k) k_1).det
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: case mp
X Y : CompHaus
f : X ⟶ Y
⊢ Epi f → Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
dsimp [Function.Surjective]

Goal state after:
case mp
X Y : CompHaus
f : X ⟶ Y
⊢ Epi f → ∀ (b : ↑Y.toTop), ∃ a, (ConcreteCategory.hom f) a = b
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
⊢ ∀ (i' : Set X),
    IsClosed[inst✝] i' ∧ IsCompact i' → ∃ i, (∞ ∈ i ∧ IsOpen[instTopologicalSpace] i) ∧ i ∩ {∞}ᶜ ⊆ some '' i'ᶜ

Tactic:
· rintro s ⟨h₁, h₂⟩
    refine ⟨_, ⟨mem_compl infty_notMem_image_coe, isOpen_compl_image_coe.2 ⟨h₁, h₂⟩⟩, ?_⟩
    simp [compl_image_coe, ← sdiff_eq]

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : MulAction G X
inst✝² : CompactlyGeneratedSpace (X × X)
inst✝¹ : T2Space X
inst✝ : ContinuousSMul G X
⊢ ProperSMul G X ↔ ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g | (g • U ∩ V).Nonempty}

Tactic:
refine ⟨fun h ↦ ProperSMul.isCompact_setOfPred_inter_nonempty, fun h ↦ ⟨?_⟩⟩
  refine isProperMap_iff_isCompact_preimage.mpr ⟨by fun_prop, fun {K} hK ↦ ?_⟩
  -- First reduce to the case `K = U × V`.
  let U := Prod.fst '' K
  let V := Prod.snd '' K
  have hU : IsCompact U := hK.image continuous_fst
  have hV : IsCompact V := hK.image continuous_snd
  suffices IsCompact ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' (U ×ˢ V)) by
    apply this.of_isClosed_subset (hK.isClosed.preimage <| by fun_prop)
    exact Set.preimage_mono Set.subset_fst_image_prod_snd_image
  apply ((h hV hU).prod hV).of_isClosed_subset
  · exact (hU.prod hV).isClosed.preimage (by fun_prop)
  · exact fun ⟨g, x⟩ ⟨hgx, hgx'⟩ ↦ ⟨⟨g • x, smul_mem_smul_set hgx', hgx⟩, hgx'⟩

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: case infty
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
s : Set (OnePoint X✝)
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
y : OnePoint X
x✝¹ : y ∈ univ
x✝ : ∞ ∈ univ
hxy : ∞ ≠ y
⊢ ∃ u v, IsOpen[instTopologicalSpace] u ∧ IsOpen[instTopologicalSpace] v ∧ ∞ ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
refine ⟨{y}ᶜ, {y}, isOpen_compl_singleton, ?_, hxy, rfl, (compl_union_self _).symm.subset,
        disjoint_compl_left⟩
      rw [OnePoint.isOpen_iff_of_notMem]
      exacts [isOpen_discrete _, hxy]

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed[inst✝¹] (s ∩ K)) → IsClosed[inst✝¹] s
s : Set X
hs :
  ∀ (K : Type u) [inst : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
    Continuous[_, inst✝¹] f → IsClosed (f ⁻¹' s)
K : Set X
hK : IsCompact K
⊢ IsClosed[inst✝¹] (Subtype.val '' Subtype.val ⁻¹' s)

Tactic:
apply hK.isClosed.isClosedMap_subtype_val

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed[inst✝¹] (s ∩ K)) → IsClosed[inst✝¹] s
s : Set X
hs :
  ∀ (K : Type u) [inst : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
    Continuous[_, inst✝¹] f → IsClosed (f ⁻¹' s)
K : Set X
hK : IsCompact K
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' s)
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mp.inr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
w : ℝ
wt : w ∈ t
zw : z ≤ w
wy : w ≤ y
⊢ w ∈ s ∩ Icc z y

Tactic:
exact ⟨(le_antisymm (wy.trans (hs.2 ys)) (ht.2 wt)).symm ▸ hs.1, zw, wy⟩

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

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a b : ℝ
ha : 0 < a
hb : 0 < b
a✝ : a ≤ b
s : Set E := ((toClosedBall b) D).support
hs : s.Finite
z : E
hz : z ∈ hs.toFinset
h₂z : ¬z = 0
⊢ ↑(((toClosedBall a) D) z) * log (a * ‖z‖⁻¹) ≤ ↑(((toClosedBall b) D) z) * log (b * ‖z‖⁻¹)

Tactic:
have := (toClosedBall_support_subset_closedBall D (hs.mem_toFinset.1 hz))
        rw [toClosedBall_eval_within _ this]
        by_cases h₃z : z ∈ closedBall 0 |a|
        · rw [toClosedBall_eval_within _ h₃z]
          gcongr
          exact Int.cast_nonneg (hD z)
        · simp only [h₃z, not_false_eq_true, apply_eq_zero_of_notMem, Int.cast_zero, zero_mul,
            ge_iff_le]
          apply mul_nonneg (Int.cast_nonneg (hD z)) (log_nonneg _)
          apply (le_mul_inv_iff₀ (norm_pos_iff.mpr h₂z)).2
          simp_all [abs_of_pos hb]

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

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
f : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f
hr : 1 ≤ r
h₃r : 0 < r
this : ∀ (z : E), 0 ≤ ↑(((toClosedBall r) f) z) * log (r * ‖z‖⁻¹)
⊢ 0 ≤ ↑(f 0)

Tactic:
by simpa using h 0

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

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
f₁ f₂ : locallyFinsupp E ℤ
r : ℝ
h : f₁ ≤ f₂
hr : 1 ≤ r
⊢ logCounting f₁ r ≤ logCounting f₂ r

Tactic:
by
  rw [← sub_nonneg] at h ⊢
  simpa using logCounting_nonneg h hr

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
φ : ℝ → ℝ
φm : MonotoneOn φ (Icc 0 s)
φst : φ '' Icc 0 s = Icc 0 t
hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)
hf : HasUnitSpeedOn f (φ '' Icc 0 s)
x✝ x : ℝ
xs : x ∈ Icc 0 s
hx : φ x = 0
this : MapsTo φ (Icc 0 s) (Icc 0 t)
⊢ 0 ≤ 0 ∧ 0 ≤ s

Tactic:
exact ⟨le_rfl, hs⟩

Goal state after:
Module: Mathlib.Analysis.Convex.BetweenList

Goal state before:
pp: case refine_2
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
l : List P
hl : l ≠ []
h : List.Sbtw R l
⊢ ∃ l', l'.SortedLT ∧ map (⇑(lineMap (l.head hl) (l.getLast hl))) l' = l ∧ (l.length = 1 ∨ l.head hl ≠ l.getLast hl)

Tactic:
· rw [List.Sbtw, ← exists_map_eq_of_sorted_nonempty_iff_wbtw hl] at h
    rcases h with ⟨⟨l', hl's, hl'l⟩, hp⟩
    refine ⟨l', ?_, hl'l, ?_⟩
    · rw [← hl'l] at hp
      have hp' : l'.Pairwise (· ≠ ·) := hp.of_map _ (by simp)
      exact ((pairwise_and_iff.2 ⟨hl's.pairwise, hp'⟩).imp lt_iff_le_and_ne.2).sortedLT
    · cases l with
      | nil => simp at hl
      | cons head tail =>
        simp only [length_cons, add_eq_right, length_eq_zero_iff, head_cons]
        cases tail with
        | nil => simp
        | cons head2 tail =>
          simp only [reduceCtorEq, false_or]
          rw [pairwise_cons] at hp
          refine hp.1 ((head :: head2 :: tail).getLast hl) ?_
          simp

Goal state after:
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: α : Type v
inst✝¹ : DecidableEq α
ι : Type u
t : ι → Finset α
inst✝ : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val✝ : Fintype ι
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι],
      (∀ (s : Finset ι), #s ≤ #(s.biUnion t)) →
        ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = n + 1
⊢ ∀ (ι' : Type u) [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x

Tactic:
intro ι' _ _ hι' ht'

Goal state after:
α : Type v
inst✝² : DecidableEq α
ι : Type u
t : ι → Finset α
inst✝¹ : Finite ι
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
val✝ : Fintype ι
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {ι : Type u} {t : ι → Finset α} [Finite ι],
      (∀ (s : Finset ι), #s ≤ #(s.biUnion t)) →
        ∀ (val : Fintype ι), Fintype.card ι = m → ∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
hn : Fintype.card ι = n + 1
ι' : Type u
inst✝ : Fintype ι'
t'✝ : ι' → Finset α
hι' : Fintype.card ι' ≤ n
ht' : ∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t'✝)
⊢ ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t'✝ x
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i
⊢ Sbtw R ((Finset.affineCombination R s p) w₁) ((Finset.affineCombination R s p) w)
    ((Finset.affineCombination R s p) w₂)

Tactic:
change ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i at hr

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
ι : Type u_6
p : ι → P
ha : AffineIndependent R p
w w₁ w₂ : ι → R
s : Finset ι
hw : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
i : ι
his : i ∈ s
r : R
hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1
hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i
⊢ Sbtw R ((Finset.affineCombination R s p) w₁) ((Finset.affineCombination R s p) w)
    ((Finset.affineCombination R s p) w₂)
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
s : Simplex R P 1
p : P
⊢ p ∈ s.closedInterior ↔ Wbtw R (s.points 0) p (s.points 1)

Tactic:
by
  rw [closedInterior_eq_affineSegment, Wbtw]

Goal state after:
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: case mpr
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
⊢ #s ≤ #(s.biUnion t)

Tactic:
rw [← Finset.card_image_of_injective s hf₁]

Goal state after:
case mpr
ι : Type u
α : Type v
inst✝ : DecidableEq α
t : ι → Finset α
f : ι → α
hf₁ : Injective f
hf₂ : ∀ (x : ι), f x ∈ t x
s : Finset ι
⊢ #(image f s) ≤ #(s.biUnion t)
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
h : ofSet s = PEquiv.refl α
⊢ s = Set.univ

Tactic:
rw [Set.eq_univ_iff_forall]
    intro
    rw [← mem_ofSet_self_iff, h]
    exact rfl

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
x : α
y : β
h1 : y = b
h2 : ¬x = a
⊢ ¬a = x

Tactic:
exact Ne.symm h2

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Permutation

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Fintype n
v : n → R
inst✝ : CommRing R
⊢ v ᵥ* Perm.permMatrix R σ = v ∘ ⇑(Equiv.symm σ)

Tactic:
by
  ext j
  simp [vecMul_eq_sum, Pi.single, Function.update, ← Equiv.symm_apply_eq σ]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Stochastic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
M : Matrix n n R
x : n → R
hM : M ∈ colStochastic R n
hx : ∀ (i : n), 0 ≤ x i
⊢ ∀ (j : n), 0 ≤ (M *ᵥ x) j

Tactic:
intro j
  simp only [Matrix.mulVec, dotProduct]
  apply Finset.sum_nonneg
  intro k _
  refine Left.mul_nonneg ?_ (hx k)
  exact nonneg_of_mem_colStochastic hM

Goal state after: