mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
m : Matrix (Fin 2) (Fin 2) R
hm : (m 0 0 + m 1 1) ^ 2 - 4 * m.det < 0
hc : m 0 1 * m 1 0 = 0
⊢ False

Tactic:
det_fin_two,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
m : Matrix (Fin 2) (Fin 2) R
hm : (m 0 0 + m 1 1) ^ 2 - 4 * (m 0 0 * m 1 1 - m 0 1 * m 1 0) < 0
hc : m 0 1 * m 1 0 = 0
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
m : Matrix (Fin 2) (Fin 2) R
hm : (m 0 0 + m 1 1) ^ 2 - 4 * (m 0 0 * m 1 1 - m 0 1 * m 1 0) < 0
hc : m 0 1 * m 1 0 = 0
⊢ False

Tactic:
hc

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
m : Matrix (Fin 2) (Fin 2) R
hm : (m 0 0 + m 1 1) ^ 2 - 4 * (m 0 0 * m 1 1 - 0) < 0
hc : m 0 1 * m 1 0 = 0
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det : det g = 1 ∨ det g = -1
hg10 : ↑g 1 0 = 0
hg00 : ↑g 0 0 = ↑g 1 1
hg01 : ↑g 0 1 ≠ 0
⊢ (↑g).det = ↑g 1 1 ^ 2

Tactic:
det_fin_two,

Goal state after:
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det : det g = 1 ∨ det g = -1
hg10 : ↑g 1 0 = 0
hg00 : ↑g 0 0 = ↑g 1 1
hg01 : ↑g 0 1 ≠ 0
⊢ ↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0 = ↑g 1 1 ^ 2
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mp
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det : det g = 1 ∨ det g = -1
hg10 : ↑g 1 0 = 0
hg00 : ↑g 0 0 = ↑g 1 1
hg01 : ↑g 0 1 ≠ 0
this : ↑g 1 1 ^ 2 = 1
⊢ (∃ x, x ≠ 0 ∧ g = upperRightHom x) ∨ ∃ x, x ≠ 0 ∧ g = -upperRightHom x

Tactic:
apply (sq_eq_one_iff.mp this).imp

Goal state after:
case mp.f
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det : det g = 1 ∨ det g = -1
hg10 : ↑g 1 0 = 0
hg00 : ↑g 0 0 = ↑g 1 1
hg01 : ↑g 0 1 ≠ 0
this : ↑g 1 1 ^ 2 = 1
⊢ ↑g 1 1 = 1 → ∃ x, x ≠ 0 ∧ g = upperRightHom x

case mp.g
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det : det g = 1 ∨ det g = -1
hg10 : ↑g 1 0 = 0
hg00 : ↑g 0 0 = ↑g 1 1
hg01 : ↑g 0 1 ≠ 0
this : ↑g 1 1 ^ 2 = 1
⊢ ↑g 1 1 = -1 → ∃ x, x ≠ 0 ∧ g = -upperRightHom x
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inr.inr.inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
xl : Y → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
hgb : ∀ (y : Y), g y ≤ b
hb' : ¬∃ x, f x = b
hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {b})
dg : Y →ᵇ ℝ
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Iic c)
dgb : EqOn (⇑dg) (Function.const Y (b - c)) (⇑g ⁻¹' {b})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (b - c)
hgf : ∀ (x : X), (g - dg) (e x) = f x
y : Y
hyb : (g - dg) y < b
xu : X
hyxu : (g - dg) y < f xu
right✝ : f xu ≤ b
hc : g y ≤ c
⊢ ∃ x₁ x₂, (g - dg) y ∈ Icc (f x₁) (f x₂)

Tactic:
· refine ⟨xl y, xu, ?_, hyxu.le⟩
    simp [dg0 (Or.inr hc), hxl]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
x : P
hne : x ≠ c
⊢ (R * R / (R ^ 2 / dist x c * dist x c)) ^ 2 • (x -ᵥ c) +ᵥ c = x

Tactic:
div_mul_cancel₀ _ (dist_ne_zero.2 hne),

Goal state after:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
x : P
hne : x ≠ c
⊢ (R * R / R ^ 2) ^ 2 • (x -ᵥ c) +ᵥ c = x
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
⊢ dist ↑z ↑(w.center r) ^ 2 = 2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2

Tactic:
have H : 2 * z.im * w.im ≠ 0 := by positivity
  simp only [Complex.dist_eq, Complex.sq_norm, normSq_apply, coe_re, coe_im, center_re, center_im,
    cosh_dist', mul_div_cancel₀ _ H, sub_sq z.im, mul_pow, Real.cosh_sq, sub_re, sub_im, mul_sub, ←
    sq]
  ring

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

Goal state before:
pp: ⊢ StrictMono fun x ↦ sinh x - x

Tactic:
refine strictMono_of_odd_strictMonoOn_nonneg (fun x => by simp; abel) ?_

Goal state after:
⊢ StrictMonoOn (fun x ↦ sinh x - x) (Ici 0)
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: case mp
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Mono f
x₁ x₂ : ↑X.toTop
h : (ConcreteCategory.hom f) x₁ = (ConcreteCategory.hom f) x₂
g₁ : X ⟶ X := ofHom P { toFun := fun x ↦ x₁, continuous_toFun := ⋯ }
g₂ : X ⟶ X := ofHom P { toFun := fun x ↦ x₂, continuous_toFun := ⋯ }
this : g₁ ≫ f = g₂ ≫ f
⊢ x₁ = x₂

Tactic:
exact CategoryTheory.congr_fun ((cancel_mono _).mp this) x₁

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

Goal state before:
pp: case mp
z : ℍ
r : ℝ
w : ℍ
hw : w ∈ ball z r
⊢ ↑w ∈ ball (↑(z.center r)) (z.im * Real.sinh r)

Tactic:
exact dist_lt_iff_dist_coe_center_lt.1 hw

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

Goal state before:
pp: X : Type u_1
x₁ x₂ : X
⊢ ↑x₁ = ↑x₂ ↔ x₁ = x₂

Tactic:
rw [iff_eq_eq]
  exact Option.some.injEq x₁ x₂

Goal state after:
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
h_proper : ProperSMul G X
inst✝ : T1Space G
⊢ T2Space X

Tactic:
let f := fun x : X ↦ ((1 : G), x)
  have proper_f : IsProperMap f := by
    refine IsClosedEmbedding.isProperMap ⟨isEmbedding_prodMkRight 1, ?_⟩
    have : range f = ({1} ×ˢ univ) := by simp [f, Set.singleton_prod]
    rw [this]
    exact isClosed_singleton.prod isClosed_univ
  rw [t2_iff_isClosed_diagonal]
  let g := fun gx : G × X ↦ (gx.1 • gx.2, gx.2)
  have proper_g : IsProperMap g := (properSMul_iff G X).1 h_proper
  have : g ∘ f = Function.diag := by ext x <;> simp [f, g]
  have range_gf : range (g ∘ f) = diagonal X := by simp [this]
  rw [← range_gf]
  exact (proper_g.comp proper_f).isClosed_range

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
f : Filter (OnePoint X)
⊢ f ≤ 𝓝 ∞ ↔ ∀ (s : Set X), IsClosed[inst✝] s → IsCompact s → some '' sᶜ ∪ {∞} ∈ f

Tactic:
by
  simp only [hasBasis_nhds_infty.ge_iff, and_imp]

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

Goal state before:
pp: X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : UCompactlyGeneratedSpace X
f : X → Y
hf : Continuous[tX, tY] f
ht : tY = coinduced f tX
s : Set Y
h : ∀ (S : CompHaus) (f : C(↑S.toTop, Y)), IsClosed (⇑f ⁻¹' s)
⊢ IsClosed[tY] s

Tactic:
ht,

Goal state after:
X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : UCompactlyGeneratedSpace X
f : X → Y
hf : Continuous[tX, tY] f
ht : tY = coinduced f tX
s : Set Y
h : ∀ (S : CompHaus) (f : C(↑S.toTop, Y)), IsClosed (⇑f ⁻¹' s)
⊢ IsClosed[coinduced f tX] s
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
⊢ proximity (∑ a ∈ s, f a) ⊤ ≤ ∑ a ∈ s, proximity (f a) ⊤ + fun x ↦ log ↑s.card

Tactic:
simp only [proximity_top, Finset.sum_apply]
  intro r
  have h₂f : ∀ i ∈ s, CircleIntegrable (log⁺ ‖f i ·‖) 0 r :=
    fun i hi ↦ MeromorphicOn.circleIntegrable_posLog_norm (fun x hx ↦ hf i hi x)
  simp only [Pi.add_apply, Finset.sum_apply]
  calc circleAverage (log⁺ ‖∑ c ∈ s, f c ·‖) 0 r
    _ ≤ circleAverage (∑ c ∈ s, log⁺ ‖f c ·‖ + log s.card) 0 r := by
      apply circleAverage_mono
      · apply (Meromorphic.fun_sum hf).meromorphicOn.circleIntegrable_posLog_norm
      · fun_prop
      · intro x hx
        rw [add_comm]
        apply posLog_norm_sum_le
    _ = ∑ c ∈ s, circleAverage (log⁺ ‖f c ·‖) 0 r + log s.card := by
      nth_rw 2 [← circleAverage_const (log s.card) 0 r]
      rw [← circleAverage_sum h₂f, ← circleAverage_add (CircleIntegrable.sum s h₂f)
        (circleIntegrable_const (log s.card) 0 r)]
      congr 1
      ext x
      simp

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

Goal state before:
pp: case e_a
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ ∑ᶠ (z : E), (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹) =
    ∑ᶠ (z : E), ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹) + ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)

Tactic:
rw [finsum_eq_sum_of_support_subset (s := h₁s.toFinset)]

Goal state after:
case e_a
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ ∑ i ∈ h₁s.toFinset, (↑(((toClosedBall r) D₁) i) + ↑(((toClosedBall r) D₂) i)) * log (r * ‖i‖⁻¹) =
    ∑ᶠ (z : E), ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹) + ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)

case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case e_a
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ ∑ i ∈ h₁s.toFinset, (↑(((toClosedBall r) D₁) i) + ↑(((toClosedBall r) D₂) i)) * log (r * ‖i‖⁻¹) =
    ∑ᶠ (z : E), ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹) + ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)

pp: case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

Tactic:
rw [finsum_eq_sum_of_support_subset (s := h₁s.toFinset)]

Goal state after:
case e_a
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ ∑ i ∈ h₁s.toFinset, (↑(((toClosedBall r) D₁) i) + ↑(((toClosedBall r) D₂) i)) * log (r * ‖i‖⁻¹) =
    ∑ i ∈ h₁s.toFinset, ↑(((toClosedBall r) D₁) i) * log (r * ‖i‖⁻¹) +
      ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)

case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case e_a
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ ∑ i ∈ h₁s.toFinset, (↑(((toClosedBall r) D₁) i) + ↑(((toClosedBall r) D₂) i)) * log (r * ‖i‖⁻¹) =
    ∑ i ∈ h₁s.toFinset, ↑(((toClosedBall r) D₁) i) * log (r * ‖i‖⁻¹) +
      ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)

pp: case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

pp: case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

Tactic:
rw [finsum_eq_sum_of_support_subset (s := h₁s.toFinset)]

Goal state after:
case e_a
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ ∑ i ∈ h₁s.toFinset, (↑(((toClosedBall r) D₁) i) + ↑(((toClosedBall r) D₂) i)) * log (r * ‖i‖⁻¹) =
    ∑ i ∈ h₁s.toFinset, ↑(((toClosedBall r) D₁) i) * log (r * ‖i‖⁻¹) +
      ∑ i ∈ h₁s.toFinset, ↑(((toClosedBall r) D₂) i) * log (r * ‖i‖⁻¹)

case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

pp: case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

pp: case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

Tactic:
rw [finsum_eq_sum_of_support_subset (s := h₁s.toFinset)]

Goal state after:
case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset
Module: Mathlib.Analysis.Convex.AmpleSet

Goal state before:
pp: case inl
F : Type u_1
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ s
hx : (convexHull ℝ) (connectedComponentIn s x) = univ
⊢ univ ⊆ (convexHull ℝ) (connectedComponentIn (s ∪ t) x)

Tactic:
← hx

Goal state after:
case inl
F : Type u_1
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ s
hx : (convexHull ℝ) (connectedComponentIn s x) = univ
⊢ (convexHull ℝ) (connectedComponentIn s x) ⊆ (convexHull ℝ) (connectedComponentIn (s ∪ t) x)
Module: Mathlib.Analysis.Convex.AmpleSet

Goal state before:
pp: case inr
F : Type u_1
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ t
hx : (convexHull ℝ) (connectedComponentIn t x) = univ
⊢ univ ⊆ (convexHull ℝ) (connectedComponentIn (s ∪ t) x)

Tactic:
← hx

Goal state after:
case inr
F : Type u_1
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
h : x ∈ t
hx : (convexHull ℝ) (connectedComponentIn t x) = univ
⊢ (convexHull ℝ) (connectedComponentIn t x) ⊆ (convexHull ℝ) (connectedComponentIn (s ∪ t) x)
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.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 ι
x : ι
hx : x ∈ s
⊢ ∀ (x_1 : x ∈ (↑s)ᶜ), ⟨x, ⋯⟩ ∉ s'

Tactic:
hc

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 ι
x : ι
hx : x ∈ s
hc : x ∈ (↑s)ᶜ
⊢ ⟨x, ⋯⟩ ∉ s'
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
h : Wbtw R x y z
f : P →ᵃ[R] P'
⊢ Wbtw R (f x) (f y) (f z)

Tactic:
rw [Wbtw, ← affineSegment_image]
  exact Set.mem_image_of_mem _ h

Goal state after:
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
x y z p : P
⊢ Sbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ↔ Sbtw R x y z

Tactic:
by
  rw [Sbtw, Sbtw, wbtw_const_vsub_iff, (vsub_right_injective p).ne_iff,
    (vsub_right_injective p).ne_iff]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Konig

Goal state before:
pp: case h
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
h✝ : Nonempty J
this : IsCofiltered J
X Y : J
hX : X ∈ G
hY : Y ∈ G
f : X ⟶ Y
hf : ⟨X, ⟨Y, ⟨hX, ⟨hY, f⟩⟩⟩⟩ ∈ H
⊢ (ConcreteCategory.hom (F.map (IsCofiltered.infTo G H hX ≫ f))) ⋯.some =
    (ConcreteCategory.hom (F.map (IsCofiltered.infTo G H hY))) ⋯.some

Tactic:
@IsCofiltered.infTo_commutes _ _ _ G H

Goal state after:
case h
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
h✝ : Nonempty J
this : IsCofiltered J
X Y : J
hX : X ∈ G
hY : Y ∈ G
f : X ⟶ Y
hf : ⟨X, ⟨Y, ⟨hX, ⟨hY, f⟩⟩⟩⟩ ∈ H
⊢ (ConcreteCategory.hom (F.map (IsCofiltered.infTo G H ?h.mY))) ⋯.some =
    (ConcreteCategory.hom (F.map (IsCofiltered.infTo G H hY))) ⋯.some

case h.mY
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
h✝ : Nonempty J
this : IsCofiltered J
X Y : J
hX : X ∈ G
hY : Y ∈ G
f : X ⟶ Y
hf : ⟨X, ⟨Y, ⟨hX, ⟨hY, f⟩⟩⟩⟩ ∈ H
⊢ Y ∈ G

case h.mf
J : Type u
inst✝¹ : SmallCategory J
F : J ⥤ TopCat
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), Nonempty ↑(F.obj j)
G : Finset J
H : Finset (FiniteDiagramArrow G)
h✝ : Nonempty J
this : IsCofiltered J
X Y : J
hX : X ∈ G
hY : Y ∈ G
f : X ⟶ Y
hf : ⟨X, ⟨Y, ⟨hX, ⟨hY, f⟩⟩⟩⟩ ∈ H
⊢ ⟨X, ⟨Y, ⟨hX, ⟨?h.mY, f⟩⟩⟩⟩ ∈ H