mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
⊢ circleAverage (fun x ↦ log ‖x - a‖) 0 1 = 0

Tactic:
by
  -- Observing that the problem is rotation invariant, we rotate by an angle of `ζ = - arg a` and
  -- reduce the problem to the case where `a = 1`. The integral can then be evaluated by a direct
  -- computation.
  simp only [circleAverage, mul_inv_rev, smul_eq_mul, mul_eq_zero, inv_eq_zero, OfNat.ofNat_ne_zero,
    or_false]
  right
  obtain ⟨ζ, hζ⟩ : ∃ ζ, a⁻¹ = circleMap 0 1 ζ := by simp [Set.exists_range_iff.1, h]
  calc ∫ x in 0..(2 * π), log ‖circleMap 0 1 x - a‖
  _ = ∫ x in 0..(2 * π), log ‖(circleMap 0 1 ζ) * (circleMap 0 1 x - a)‖ := by
    simp
  _ = ∫ x in 0..(2 * π), log ‖circleMap 0 1 (ζ + x) - (circleMap 0 1 ζ) * a‖ := by
    simp [mul_sub, circleMap, add_mul, Complex.exp_add]
  _ = ∫ x in 0..(2 * π), log ‖circleMap 0 1 (ζ + x) - 1‖ := by
    simp [← hζ, inv_mul_cancel₀ (by aesop : a ≠ 0)]
  _ = ∫ x in 0..(2 * π), log ‖circleMap 0 1 x - 1‖ := by
    have : Function.Periodic (log ‖circleMap 0 1 · - 1‖) (2 * π) :=
      fun x ↦ by simp [periodic_circleMap 0 1 x]
    have := this.intervalIntegral_add_eq (t := 0) (s := ζ)
    simp_all [integral_comp_add_left (log ‖circleMap 0 1 · - 1‖)]
  _ = ∫ x in 0..(2 * π), log (4 * sin (x / 2) ^ 2) / 2 := by
    apply integral_congr
    intro x hx
    simp only
    rw [Complex.norm_def, log_sqrt (circleMap 0 1 x - 1).normSq_nonneg]
    congr
    calc Complex.normSq (circleMap 0 1 x - 1)
    _ = (cos x - 1) * (cos x - 1) + sin x * sin x := by
      simp [circleMap, Complex.normSq_apply]
    _ = sin x ^ 2 + cos x ^ 2 + 1 - 2 * cos x := by
      ring
    _ = 2 - 2 * cos x := by
      rw [sin_sq_add_cos_sq]
      norm_num
    _ = 2 - 2 * cos (2 * (x / 2)) := by
      rw [← mul_div_assoc]
      simp
    _ = 4 - 4 * cos (x / 2) ^ 2 := by
      rw [cos_two_mul]
      ring
    _ = 4 * sin (x / 2) ^ 2 := by
      nth_rw 1 [← mul_one 4, ← sin_sq_add_cos_sq (x / 2)]
      ring
  _ = 0 := circleAverage_log_norm_sub_const₁_integral

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

Goal state before:
pp: a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ circleAverage (fun z ↦ log ‖↑R * (z + ↑R⁻¹ * (c - a))‖) 0 1 =
    circleAverage (fun z ↦ log ‖R‖ + log ‖z + ↑R⁻¹ * (c - a)‖) 0 1

Tactic:
apply circleAverage_congr_codiscreteWithin _ (zero_ne_one' ℝ).symm
    have : {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0} ∈ codiscreteWithin (Metric.sphere (0 : ℂ) |1|) := by
      apply codiscreteWithin_iff_locallyFiniteComplementWithin.2
      intro z hz
      use Set.univ
      simp only [univ_mem, abs_one, Complex.ofReal_inv, ne_eq, norm_eq_zero, Set.univ_inter,
        true_and]
      apply Set.Subsingleton.finite
      intro z₁ hz₁ z₂ hz₂
      simp_all only [ne_eq, abs_one, mem_sphere_iff_norm, sub_zero, Set.mem_sdiff,
        Set.mem_ofPred_eq, Decidable.not_not]
      rw [add_eq_zero_iff_eq_neg.1 hz₁.2, add_eq_zero_iff_eq_neg.1 hz₂.2]
    filter_upwards [this] with z hz
    rw [norm_mul, log_mul (norm_ne_zero_iff.2 (Complex.ofReal_ne_zero.mpr hR)) hz]
    simp

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

Goal state before:
pp: f : ℂ → ℂ
U : Set ℂ
c₀ : ℝ
h₁f : AnalyticOnNhd ℂ f U
h₂f : ∀ x ∈ U, (f x).im = c₀
h₁U : IsOpen U
h₂U : IsConnected U
z₀ : ℂ
h✝ : z₀ ∈ U
h₅ : ¬∃ c, ∀ x ∈ U, f x = c
⊢ False

Tactic:
grind [not_isOpen_singleton (c₀ : ℝ), (by aesop : (im '' f '' U) = { c₀ }), isOpenMap_im
    (f '' U) ((h₁f.is_constant_or_isOpen h₂U.isPreconnected).resolve_left h₅ U (by tauto) h₁U)]

Goal state after:
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
hz : derivative P ≠ 0 ∧ eval z (derivative P) = 0
⊢ z ∈ (convexHull ℝ) (P.rootSet ℂ)

Tactic:
eq_centerMass_of_eval_derivative_eq_zero h₀ hz.2

Goal state after:
P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
hz : derivative P ≠ 0 ∧ eval z (derivative P) = 0
⊢ P.roots.toFinset.centerMass (P.derivRootWeight z) id ∈ (convexHull ℝ) (P.rootSet ℂ)
Module: Mathlib.Analysis.Complex.RiemannMapping

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
z : ℂ
hz : z ∈ U
⊢ deriv (fun z ↦ ↑ε / (f z - x)) z ≠ 0

Tactic:
have hdz : DifferentiableAt ℂ f z := differentiableAt_of_deriv_ne_zero (hdf z hz)

Goal state after:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
hfx : ∀ z ∈ U, f z ≠ x
z : ℂ
hz : z ∈ U
hdz : DifferentiableAt ℂ f z
⊢ deriv (fun z ↦ ↑ε / (f z - x)) z ≠ 0
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: a : ℝ
⊢ (↑a).sqrt.re = √a

Tactic:
by
  simp only [cpow_inv_two_re, norm_real, Real.norm_eq_abs, ofReal_re, Complex.sqrt]
  grind

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

Goal state before:
pp: case refine_2
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
this✝ : NormedSpace ℝ E
this : IsScalarTower ℝ 𝕜 E
g : E → E := fun x ↦ ‖x‖⁻¹ • x
⊢ ∀ (x : E), 1 ≤ ‖x‖ → ¬x = 0

Tactic:
exact fun x hx ↦ norm_pos_iff.mp <| one_pos.trans_le hx

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : (↑g).trace = 0
hc : ↑g 1 0 ≠ 0
⊢ dist (↑z) (-↑(↑g 1 1) / ↑(↑g 1 0)) = √(-(↑g).det / ↑g 1 0 ^ 2) ↔
    dist (↑z) (-↑(↑g 1 1) / ↑(↑g 1 0)) = √(-(↑g).det) / |↑g 1 0|

pp: case hx
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : (↑g).trace = 0
hc : ↑g 1 0 ≠ 0
⊢ 0 ≤ -(↑g).det / ↑g 1 0 ^ 2

pp: case hy
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : (↑g).trace = 0
hc : ↑g 1 0 ≠ 0
⊢ 0 ≤ dist (↑z) (-↑(↑g 1 1) / ↑(↑g 1 0))

Tactic:
Real.sqrt_div',

Goal state after:
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : (↑g).trace = 0
hc : ↑g 1 0 ≠ 0
⊢ dist (↑z) (-↑(↑g 1 1) / ↑(↑g 1 0)) = √(-(↑g).det) / √(↑g 1 0 ^ 2) ↔
    dist (↑z) (-↑(↑g 1 1) / ↑(↑g 1 0)) = √(-(↑g).det) / |↑g 1 0|

case hy
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : (↑g).trace = 0
hc : ↑g 1 0 ≠ 0
⊢ 0 ≤ ↑g 1 0 ^ 2

case hx
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : (↑g).trace = 0
hc : ↑g 1 0 ≠ 0
⊢ 0 ≤ -(↑g).det / ↑g 1 0 ^ 2

case hy
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : (↑g).trace = 0
hc : ↑g 1 0 ≠ 0
⊢ 0 ≤ dist (↑z) (-↑(↑g 1 1) / ↑(↑g 1 0))
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
⊢ ∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖

Tactic:
by
  have h3 : (0 : ℝ) < 3 := by norm_num1
  have h23 : 0 < (2 / 3 : ℝ) := by norm_num1
  -- In the trivial case `f = 0`, we take `g = 0`
  rcases eq_or_ne f 0 with (rfl | hf)
  · simp
  replace hf : 0 < ‖f‖ := norm_pos_iff.2 hf
  /- Otherwise, the closed sets `e '' f ⁻¹' (Iic (-‖f‖ / 3))` and `e '' f ⁻¹' (Ici (‖f‖ / 3))`
    are disjoint, hence by Urysohn's lemma there exists a function `g` that is equal to `-‖f‖ / 3`
    on the former set and is equal to `‖f‖ / 3` on the latter set. This function `g` satisfies the
    assertions of the lemma. -/
  have hf3 : -‖f‖ / 3 < ‖f‖ / 3 := (div_lt_div_iff_of_pos_right h3).2 (Left.neg_lt_self hf)
  have hc₁ : IsClosed (e '' f ⁻¹' Iic (-‖f‖ / 3)) :=
    he.isClosedMap _ (isClosed_Iic.preimage f.continuous)
  have hc₂ : IsClosed (e '' f ⁻¹' Ici (‖f‖ / 3)) :=
    he.isClosedMap _ (isClosed_Ici.preimage f.continuous)
  have hd : Disjoint (e '' f ⁻¹' Iic (-‖f‖ / 3)) (e '' f ⁻¹' Ici (‖f‖ / 3)) := by
    refine disjoint_image_of_injective he.injective (Disjoint.preimage _ ?_)
    rwa [Iic_disjoint_Ici, not_le]
  rcases exists_bounded_mem_Icc_of_closed_of_le hc₁ hc₂ hd hf3.le with ⟨g, hg₁, hg₂, hgf⟩
  refine ⟨g, ?_, ?_⟩
  · refine (norm_le <| div_nonneg hf.le h3.le).mpr fun y => ?_
    simpa [abs_le, neg_div] using hgf y
  · refine (dist_le <| mul_nonneg h23.le hf.le).mpr fun x => ?_
    have hfx : -‖f‖ ≤ f x ∧ f x ≤ ‖f‖ := by
      simpa only [Real.norm_eq_abs, abs_le] using f.norm_coe_le_norm x
    rcases le_total (f x) (-‖f‖ / 3) with hle₁ | hle₁
    · calc
        |g (e x) - f x| = -‖f‖ / 3 - f x := by
          rw [hg₁ (mem_image_of_mem _ hle₁), Function.const_apply,
            abs_of_nonneg (sub_nonneg.2 hle₁)]
        _ ≤ 2 / 3 * ‖f‖ := by linarith
    · rcases le_total (f x) (‖f‖ / 3) with hle₂ | hle₂
      · simp only [neg_div] at *
        calc
          dist (g (e x)) (f x) ≤ |g (e x)| + |f x| := dist_le_norm_add_norm _ _
          _ ≤ ‖f‖ / 3 + ‖f‖ / 3 := (add_le_add (abs_le.2 <| hgf _) (abs_le.2 ⟨hle₁, hle₂⟩))
          _ = 2 / 3 * ‖f‖ := by linarith
      · calc
          |g (e x) - f x| = f x - ‖f‖ / 3 := by
            rw [hg₂ (mem_image_of_mem _ hle₂), abs_sub_comm, Function.const_apply,
              abs_of_nonneg (sub_nonneg.2 hle₂)]
          _ ≤ 2 / 3 * ‖f‖ := by linarith

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

Goal state before:
pp: case mp.«0».«0»
R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
hP : C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0
hb : ↑g 0 1 = 0
hc : ↑g 1 0 = 0
hd : ↑g 1 1 = ↑g 0 0
⊢ (Matrix.scalar (Fin 2)) (↑g 0 0) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [hb, hc, hd]

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

Goal state before:
pp: case mp.«0».«1»
R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
hP : C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0
hb : ↑g 0 1 = 0
hc : ↑g 1 0 = 0
hd : ↑g 1 1 = ↑g 0 0
⊢ (Matrix.scalar (Fin 2)) (↑g 0 0) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [hb, hc, hd]

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

Goal state before:
pp: case mp.«1».«0»
R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
hP : C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0
hb : ↑g 0 1 = 0
hc : ↑g 1 0 = 0
hd : ↑g 1 1 = ↑g 0 0
⊢ (Matrix.scalar (Fin 2)) (↑g 0 0) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [hb, hc, hd]

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

Goal state before:
pp: case mp.«1».«1»
R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
hP : C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0
hb : ↑g 0 1 = 0
hc : ↑g 1 0 = 0
hd : ↑g 1 1 = ↑g 0 0
⊢ (Matrix.scalar (Fin 2)) (↑g 0 0) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [hb, hc, hd]

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

Goal state before:
pp: case refine_2
K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : ↑g = 0 + m
hm0 : m ≠ 0
hmsq : m ^ 2 = 0
ha : a = 0
⊢ (↑(g ^ 2)).det = 0

Tactic:
zero_add

Goal state after:
case refine_2
K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : ↑g = m
hm0 : m ≠ 0
hmsq : m ^ 2 = 0
ha : a = 0
⊢ (↑(g ^ 2)).det = 0
Module: Mathlib.RingTheory.Complex

Goal state before:
pp: z : ℂ
i j : Fin 2
⊢ (leftMulMatrix basisOneI) z i j = !![z.re, -z.im; z.im, z.re] i j

Tactic:
rw [Algebra.leftMulMatrix_eq_repr_mul, Complex.coe_basisOneI_repr, Complex.coe_basisOneI, mul_re,
    mul_im, Matrix.of_apply]

Goal state after:
z : ℂ
i j : Fin 2
⊢ ![z.re * (![1, I] j).re - z.im * (![1, I] j).im, z.re * (![1, I] j).im + z.im * (![1, I] j).re] i =
    ![![z.re, -z.im], ![z.im, z.re]] i j
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case neg
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
⊢ (norm K) x = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L

Tactic:
norm_eq_one_of_not_module_finite h

Goal state after:
case neg
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
⊢ 1 = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
b c d : P
⊢ dist b c * dist b d ≤ 0 + dist b c * dist b d

Tactic:
zero_add

Goal state after:
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
b c d : P
⊢ dist b c * dist b d ≤ dist b c * dist b d
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: a b c : ℍ
⊢ 0 < dist ((starRingEnd ℂ) ↑b) ↑b

Tactic:
dist_pos,

Goal state after:
a b c : ℍ
⊢ (starRingEnd ℂ) ↑b ≠ ↑b
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z✝ w : ℍ
r : ℝ
z : ℍ
⊢ dist z z = 0

Tactic:
by rw [dist_eq, dist_self, zero_div, arsinh_zero, mul_zero]

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

Goal state before:
pp: case inr
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
hr₀' : 0 ≤ w.im * Real.sinh r
hzw₀ : 0 < 2 * z.im * w.im
⊢ cmp (2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + ?inr.c) (0 + ?inr.c) =
    cmp (2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2) ((w.im * Real.sinh r) ^ 2)

pp: case inr.c
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
hr₀' : 0 ≤ w.im * Real.sinh r
hzw₀ : 0 < 2 * z.im * w.im
⊢ ℝ

Tactic:
zero_add

Goal state after:
case inr
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
hr₀' : 0 ≤ w.im * Real.sinh r
hzw₀ : 0 < 2 * z.im * w.im
⊢ cmp (2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + ?inr✝) ?inr✝ =
    cmp (2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2) ((w.im * Real.sinh r) ^ 2)

case inr
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
hr₀' : 0 ≤ w.im * Real.sinh r
hzw₀ : 0 < 2 * z.im * w.im
⊢ ℝ
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed[instTopologicalSpace] (some '' s) ↔ IsClosed[inst✝] s ∧ IsCompact s

Tactic:
by
  rw [← isOpen_compl_iff, isOpen_compl_image_coe]

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

Goal state before:
pp: case fst
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
h_proper : ProperSMul G X
inst✝ : T1Space G
f : X → G × X := ⋯
proper_f : IsProperMap f
g : G × X → X × X := ⋯
proper_g : IsProperMap g
x : X
⊢ ((g ∘ f) x).1 = (Function.diag x).1

Tactic:
simp [f, g]

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

Goal state before:
pp: case snd
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
h_proper : ProperSMul G X
inst✝ : T1Space G
f : X → G × X := ⋯
proper_f : IsProperMap f
g : G × X → X × X := ⋯
proper_g : IsProperMap g
x : X
⊢ ((g ∘ f) x).2 = (Function.diag x).2

Tactic:
simp [f, g]

Goal state after:
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: case mp
X Y : CompHaus
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
⊢ False

Tactic:
have hC : IsClosed C := (isCompact_range f.hom.hom.continuous).isClosed

Goal state after:
case mp
X Y : CompHaus
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
⊢ False
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace X
inst✝² : ContinuousSMul G X
inst✝¹ : IsTopologicalGroup G
inst✝ : IsPretransitive G X
x : X
hx : IsProperMap fun g ↦ g • x
⊢ ProperSMul G X

Tactic:
constructor
  let f : G × G → G × X := Prod.map id (fun g ↦ g • x)
  have hfsurj : f.Surjective := Function.surjective_id.prodMap (surjective_smul G x)
  refine isProperMap_of_comp_of_surj (by fun_prop) (by fun_prop) ?_ hfsurj
  simpa [Function.comp_def, Prod.map_apply, mul_smul]
    using! (hx.prodMap hx).comp (ProperSMul.isProperMap_smul_pair (G := G))

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
z : X
⊢ Disjoint (𝓝 ↑z) (𝓝 ∞)

Tactic:
nhds_infty_eq,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
s : Set (OnePoint X)
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : R1Space X
z : X
⊢ Disjoint (𝓝 ↑z) (map some (coclosedCompact X) ⊔ pure ∞)
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : SequentialSpace X
s : Set X
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := ⋯
this : Tendsto OnePoint.some atTop (𝓝 ∞)
⊢ ∀ᶠ (x : ℕ) in atTop, (ULift.up ∘ OnePoint.some) x ∈ g ⁻¹' s

Tactic:
simp only [Function.comp_apply, mem_preimage, eventually_atTop]
    exact ⟨0, fun b _ ↦ hu b⟩

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

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
h : 0 ≤ D
hO : logCounting D =O[atTop] log
C : ℝ
hC : ∀ᶠ (x : ℝ) in atTop, ‖logCounting D x‖ ≤ C * ‖log x‖
N : ℕ
hCN : max C 0 < ↑N
hCN' : C < ↑N
hInf : (support D).Infinite
t : Finset E
htsub : ↑t ⊆ support D
htcard : t.card = N
D' : locallyFinsupp E ℤ := ∑ z ∈ t, single z 1
hD' : D' = ∑ z ∈ t, single z 1
w : E
hw : w ∈ t
h₁ : D w ≠ 0
h₂ : 0 ≤ D w
⊢ 1 ≤ D w

Tactic:
omega

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : ProperSpace 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
r : ℝ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
hr : 1 ≤ r
⊢ locallyFinsuppWithin.logCounting (divisor (f₁ + f₂) univ)⁻ r ≤
    locallyFinsuppWithin.logCounting ((divisor f₁ univ)⁻ + (divisor f₂ univ)⁻) r

Tactic:
exact locallyFinsuppWithin.logCounting_le
    (negPart_divisor_add_le_add h₁f₁.meromorphicOn h₁f₂.meromorphicOn) hr

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mpr
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 : ℝ
zt : z ∈ t
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
⊢ w ∈ t ∩ Icc z y → w ∈ (s ∪ t) ∩ Icc z y

Tactic:
· rintro ⟨wt, zwy⟩; exact ⟨Or.inr wt, zwy⟩

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

Goal state before:
pp: α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this✝ : DecidableEq ι
disj : Disjoint s (image (fun z ↦ ↑z) s')
this : #s' = #(s ∪ image (fun z ↦ ↑z) s') - #s
⊢ #((s ∪ image (fun z ↦ ↑z) s').biUnion t) - #(s.biUnion t) ≤ #(s'.biUnion fun x' ↦ t ↑x' \ s.biUnion t)

Tactic:
rw [← card_sdiff_of_subset]

Goal state after:
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this✝ : DecidableEq ι
disj : Disjoint s (image (fun z ↦ ↑z) s')
this : #s' = #(s ∪ image (fun z ↦ ↑z) s') - #s
⊢ #((s ∪ image (fun z ↦ ↑z) s').biUnion t \ s.biUnion t) ≤ #(s'.biUnion fun x' ↦ t ↑x' \ s.biUnion t)

α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this✝ : DecidableEq ι
disj : Disjoint s (image (fun z ↦ ↑z) s')
this : #s' = #(s ∪ image (fun z ↦ ↑z) s') - #s
⊢ s.biUnion t ⊆ (s ∪ image (fun z ↦ ↑z) s').biUnion t
Module: Mathlib.Analysis.Convex.Approximation

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
s : Set E
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hsc : IsClosed s
hφc : LowerSemicontinuousOn φ s
hφcv : ConvexOn ℝ s φ
hs : s.Nonempty
⊢ ∃ 𝓕',
    𝓕'.Countable ∧
      sSup 𝓕' = s.domRestrict φ ∧ ∀ f ∈ 𝓕', f ≤ s.domRestrict φ ∧ ∃ l c, f = s.domRestrict (⇑re ∘ ⇑l) + const (↑s) c

Tactic:
let 𝓕 := {f | f ≤ s.domRestrict φ ∧
      ∃ (l : E →L[𝕜] 𝕜) (c : ℝ), f = s.domRestrict (re ∘ l) + const s c}
    have hl : IsLUB 𝓕 (s.domRestrict φ) := by
      refine (hφcv.sSup_affine_eq (𝕜 := 𝕜) hsc hφc) ▸ isLUB_csSup ?_ ?_
      · obtain ⟨l, c, hlc⟩ := exists_affine_le_of_lt (𝕜 := 𝕜) hs.some_mem
          (by grind : φ hs.some - 1 < φ (⟨hs.some, hs.some_mem⟩ : s)) hsc hφc hφcv
        exact ⟨s.domRestrict (re ∘ l) + const s c, hlc.1, l, c, rfl⟩
      · exact (bddAbove_def.2 ⟨φ ∘ Subtype.val, fun y hy => hy.1⟩)
    have hr (f) (hf : f ∈ 𝓕) : LowerSemicontinuous f := by
      obtain ⟨l, c, hlc⟩ := hf.2
      exact Continuous.lowerSemicontinuous (hlc ▸ by fun_prop)
    obtain ⟨𝓕', h𝓕'⟩ := exists_countable_lowerSemicontinuous_isLUB hr hl
    refine ⟨𝓕', h𝓕'.2.1, h𝓕'.2.2.csSup_eq ?_, fun f hf => h𝓕'.1 hf⟩
    by_contra!
    grind [(isLUB_empty_iff.1 (this ▸ h𝓕'.2.2)) (fun x : s => φ x - 1) ⟨hs.some, hs.some_mem⟩]

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range ⇑(ConcreteCategory.hom (F.map f₂))
j₃ : J
f₃ : j₃ ⟶ j₂
⊢ range ⇑(ConcreteCategory.hom ((F.toPreimages s).map (f₂ ≫ f₁))) ⊆
    range ⇑(ConcreteCategory.hom ((F.toPreimages s).map (f₃ ≫ f₂ ≫ f₁)))

Tactic:
rintro _ ⟨⟨x, hx⟩, rfl⟩

Goal state after:
J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ : F.eventualRange j₁ = range ⇑(ConcreteCategory.hom (F.map f₂))
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx : x ∈ ⋂ f, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' s
⊢ (ConcreteCategory.hom ((F.toPreimages s).map (f₂ ≫ f₁))) ⟨x, hx⟩ ∈
    range ⇑(ConcreteCategory.hom ((F.toPreimages s).map (f₃ ≫ f₂ ≫ f₁)))
Module: Mathlib.Analysis.Convex.DoublyStochasticMatrix

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semifield R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
M : Matrix n n R
hs : 0 ≤ 0
h₁ : ∀ (i j : n), 0 ≤ M i j
a✝ : ∀ (j : n), ∑ i, M i j = 0
i : n
h₂ : ∀ i_1 ∈ univ, M i i_1 = 0
j : n
⊢ M i j = 0 i j

Tactic:
exact h₂ _ (by simp)

Goal state after: