mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Goal state before:
pp: a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
x : ℝ
hx : x ∈ Ioo c 0
⊢ ‖Complex.exp (↑π * Complex.I * r)‖ = ‖↑x ^ r‖

Tactic:
Complex.ofReal_cpow_of_nonpos hx.2.le,

Goal state after:
a b : ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
r : ℂ
h : 0 ≤ r.re
h2 : ¬0 ∉ [[a, b]]
h' : 0 = r.re
c : ℝ
hc : c < 0
x : ℝ
hx : x ∈ Ioo c 0
⊢ ‖Complex.exp (↑π * Complex.I * r)‖ = ‖(-↑x) ^ r * Complex.exp (↑π * Complex.I * r)‖
Module: Mathlib.Analysis.SpecialFunctions.Log.PosLog

Goal state before:
pp: x : ℝ
⊢ max 0 (log x) - max 0 (-log x) = log x

Tactic:
by_cases! h : 0 ≤ log x

Goal state after:
case pos
x : ℝ
h : 0 ≤ log x
⊢ max 0 (log x) - max 0 (-log x) = log x

case neg
x : ℝ
h : log x < 0
⊢ max 0 (log x) - max 0 (-log x) = log x
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
this : ∀ᶠ (ε : ℝ) in 𝓝[<] 0, ‖cexp (↑ε * z) • f z‖ ≤ C
⊢ ‖f z‖ ≤ C

Tactic:
refine le_of_tendsto (Tendsto.mono_left ?_ nhdsWithin_le_nhds) this

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
C : ℝ
f : ℂ → E
z : ℂ
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop fun x ↦ ‖f ↑x‖
him : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
hz : 0 ≤ z.re
this : ∀ᶠ (ε : ℝ) in 𝓝[<] 0, ‖cexp (↑ε * z) • f z‖ ≤ C
⊢ Tendsto (fun c ↦ ‖cexp (↑c * z) • f z‖) (𝓝 0) (𝓝 ‖f z‖)
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:

Tactic:
log ‖circleMap 0 r θ - ρ‖
      _ ≤ |log (2 * R)| + 0 + 0 := by
        grw [← le_abs_self, norm_sub_le, hρ, two_mul, norm_circleMap_zero, abs_of_pos hr, hrR]
        simp
      _ ≤ |log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖| := by
        gcongr <;> positivity

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

Goal state before:
pp: P : ℂ[X]
z : ℂ
hP : 0 < P.degree
hz : eval z (derivative P) = 0
weight : ℂ → ℝ := P.derivRootWeight z
s : Finset ℂ := P.roots.toFinset
⊢ z = s.centerMass weight id

Tactic:
suffices ∑ x ∈ s, weight x • (z - x) = 0 by calc
    z = s.centerMass weight fun _ ↦ z := by
      rw [Finset.centerMass, ← Finset.sum_smul, inv_smul_smul₀]
      exact (sum_derivRootWeight_pos hP z).ne'
    _ = s.centerMass weight (z - ·) + s.centerMass weight id := by
      simp only [Finset.centerMass, ← smul_add, ← Finset.sum_add_distrib, id, sub_add_cancel]
    _ = s.centerMass weight id := by
      simp only [add_eq_right, Finset.centerMass, this, smul_zero]

Goal state after:
P : ℂ[X]
z : ℂ
hP : 0 < P.degree
hz : eval z (derivative P) = 0
weight : ℂ → ℝ := P.derivRootWeight z
s : Finset ℂ := P.roots.toFinset
⊢ ∑ x ∈ s, weight x • (z - x) = 0
Module: Mathlib.Analysis.Complex.TaylorSeries

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ENNReal
hf : DifferentiableOn ℂ f (Metric.eball c r)
z : ℂ
hz : z ∈ Metric.eball c r
⊢ HasSum (fun n ↦ (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)

Tactic:
by
  obtain ⟨r', hzr', hr'⟩ := exists_between (Metric.mem_eball'.mp hz)
  lift r' to NNReal using ne_top_of_lt hr'
  rw [← Metric.mem_eball', Metric.eball_coe] at hzr'
  refine hasSum_taylorSeries_on_ball ?_ hzr'
  rw [← Metric.eball_coe]
  exact hf.mono <| Metric.eball_subset_eball hr'.le

Goal state after:
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h✝ : x ∈ t
⊢ x ∈ s

Tactic:
rcases eq_or_lt_of_le hxc with (rfl | h'x)

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
x : α
h✝ : x ∈ t
hs : IsGreatest s x
ht : IsLeast t x
hxc : x ≤ x
⊢ x ∈ s

case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h✝ : x ∈ t
h'x : x < c
⊢ x ∈ s
Module: Mathlib.Order.Monotone.Union

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

Tactic:
rcases eq_or_lt_of_le hxc with (rfl | h'x)

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
hx✝ : c ∈ s ∪ t
hxc : c ≤ c
hx : c ∈ s
⊢ c ∈ t

case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
x : α
hx✝ : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ s
h'x : c < x
⊢ x ∈ t
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
⊢ ∑ᶠ (u : ℂ), ↑(D u) * (log R - log ‖c - u‖) = ∑ᶠ (u : ℂ), ↑(D u) * log (R * ‖c - u‖⁻¹) + ↑(D c) * log R

Tactic:
by_cases h : c ∈ D.support
  · have {g : ℂ → ℝ} : (fun u ↦ D u * g u).support ⊆ hD.toFinset :=
      fun x ↦ by simp +contextual
    simp only [finsum_eq_sum_of_support_subset _ this,
      Finset.sum_eq_sum_sdiff_singleton_add ((Set.Finite.mem_toFinset hD).mpr h), sub_self,
      norm_zero, log_zero, sub_zero, inv_zero, mul_zero, add_zero, add_left_inj]
    refine Finset.sum_congr rfl fun x hx ↦ ?_
    simp only [Finset.mem_sdiff, Finset.notMem_singleton] at hx
    rw [log_mul hR (inv_ne_zero (norm_ne_zero_iff.mpr (sub_eq_zero.not.2 hx.2.symm))), log_inv]
    ring
  · simp_all only [Function.mem_support, Decidable.not_not, Int.cast_zero, zero_mul, add_zero]
    refine finsum_congr fun x ↦ ?_
    by_cases h₁ : c = x
    · simp_all
    · rw [log_mul hR (inv_ne_zero (norm_ne_zero_iff.mpr (sub_eq_zero.not.2 h₁))), log_inv]
      ring

Goal state after:
Module: Mathlib.Order.Monotone.Union

Goal state before:
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
x : α
hxc : x ≤ c
h✝ : x ∈ t
⊢ x ∈ s

Tactic:
rcases eq_or_lt_of_le hxc with (rfl | h'x)

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
x : α
h✝ : x ∈ t
hs : IsGreatest s x
ht : IsLeast t x
hxc : x ≤ x
⊢ x ∈ s

case inr.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
x : α
hxc : x ≤ c
h✝ : x ∈ t
h'x : x < c
⊢ x ∈ s
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: α : 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
x : α
hx✝ : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ s
⊢ x ∈ t

Tactic:
rcases eq_or_lt_of_le hxc with (rfl | h'x)

Goal state after:
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
hx✝ : c ∈ s ∪ t
hxc : c ≤ c
hx : c ∈ s
⊢ c ∈ t

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
x : α
hx✝ : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ s
h'x : c < x
⊢ x ∈ t
Module: Mathlib.Analysis.RCLike.Sqrt

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

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

Goal state after:
a : ℝ
⊢ √((|a| + a) / 2) = √a
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case h
Y : Type v
Z : Type w
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TietzeExtension Z
ι : C(Y, Z)
r : C(Z, Y)
h : r.comp ι = ContinuousMap.id Y
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : NormalSpace X✝
s : Set X✝
hs : IsClosed[inst✝¹] s
f : C(↑s, Y)
g : C(X✝, Z)
hg : ContinuousMap.restrict s g = ι.comp f
x : ↑s
this : r.comp (ContinuousMap.restrict s g) = (r.comp ι).comp f
⊢ (ContinuousMap.restrict s (r.comp g)) x = f x

Tactic:
h,

Goal state after:
case h
Y : Type v
Z : Type w
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TietzeExtension Z
ι : C(Y, Z)
r : C(Z, Y)
h : r.comp ι = ContinuousMap.id Y
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : NormalSpace X✝
s : Set X✝
hs : IsClosed[inst✝¹] s
f : C(↑s, Y)
g : C(X✝, Z)
hg : ContinuousMap.restrict s g = ι.comp f
x : ↑s
this : r.comp (ContinuousMap.restrict s g) = (ContinuousMap.id Y).comp f
⊢ (ContinuousMap.restrict s (r.comp g)) x = f x
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case h
Y : Type v
Z : Type w
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TietzeExtension Z
ι : C(Y, Z)
r : C(Z, Y)
h : r.comp ι = ContinuousMap.id Y
X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : NormalSpace X✝
s : Set X✝
hs : IsClosed[inst✝¹] s
f : C(↑s, Y)
g : C(X✝, Z)
hg : ContinuousMap.restrict s g = ι.comp f
x : ↑s
this : r.comp (ContinuousMap.restrict s g) = f
⊢ (ContinuousMap.restrict s (r.comp g)) x = f x

Tactic:
congrm($this x)

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

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : Monoid M
inst✝² : Fact (Even (Fintype.card n))
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
⊢ ((Units.map ↑signHom).comp GeneralLinearGroup.det).comp (GeneralLinearGroup.scalar n) = 1

Tactic:
by
    ext u
    simp [← sign_pow, Even.pow_pos Fact.out]

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

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : (-g).IsElliptic
⊢ ↑(fixedPt (-g) hg) = ↑(fixedPt g ⋯)

Tactic:
simp [fixedPt, Matrix.discr_fin_two, Matrix.det_neg]

Goal state after:
g : GL (Fin 2) ℝ
hg : (-g).IsElliptic
⊢ (-↑(↑g 0 0) + ↑(↑g 1 1)) / -(2 * ↑(↑g 1 0)) = (↑(↑g 0 0) - ↑(↑g 1 1)) / (2 * ↑(↑g 1 0))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: case mp.inr
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hgt : 0 < (↑g).det
⊢ False

Tactic:
have := isElliptic_of_exists_smul_eq_self hgt hgc ⟨.I, hg _⟩
      contrapose! hg
      simp [gl_smul_eq_self_iff_eq_fixedPt hgt this, exists_ne]

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

Goal state before:
pp: case h
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / ↑N⌋
h : (↑(↑N * -n) +ᵥ z).re = ↑(-↑N * ⌊z.re / ↑N⌋) + z.re
⊢ |(↑(↑N * -n) +ᵥ z).re| ≤ ↑N

Tactic:
h,

Goal state after:
case h
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / ↑N⌋
h : (↑(↑N * -n) +ᵥ z).re = ↑(-↑N * ⌊z.re / ↑N⌋) + z.re
⊢ |↑(-↑N * ⌊z.re / ↑N⌋) + z.re| ≤ ↑N
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.Topology.TietzeExtension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ := { toFun := Subtype.val ∘ ⇑h ∘ ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ := Subtype.val ∘ ⇑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : t'.OrdConnected
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f

Tactic:
have hFt : ∀ x, F x ∈ t' := fun x => mem_image_of_mem _ (hf x)

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ := { toFun := Subtype.val ∘ ⇑h ∘ ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ := Subtype.val ∘ ⇑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : t'.OrdConnected
hFt : ∀ (x : X), F x ∈ t'
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
this : HasStrictDerivAt (num g / denom g) (↑(↑g).det / denom g ↑τ ^ 2) ↑τ
⊢ num g / denom g =ᶠ[𝓝 ↑τ] fun z ↦ ↑(g • ↑ofComplex z)

Tactic:
rw [← isOpenEmbedding_coe.map_nhds_eq, eventuallyEq_map]

Goal state after:
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
this : HasStrictDerivAt (num g / denom g) (↑(↑g).det / denom g ↑τ ^ 2) ↑τ
⊢ (num g / denom g) ∘ UpperHalfPlane.coe =ᶠ[𝓝 τ] (fun z ↦ ↑(g • ↑ofComplex z)) ∘ UpperHalfPlane.coe
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (2 * n) sinh = sinh

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih => simp_all [mul_add]

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

Goal state before:
pp: n : ℕ
⊢ iteratedDeriv (2 * n) cosh = cosh

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih => simp_all [mul_add]

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
⊢ TotallyDisconnectedSpace (Ultrafilter α)

Tactic:
by
  rw [totallyDisconnectedSpace_iff_connectedComponent_singleton]
  intro A
  simp only [Set.eq_singleton_iff_unique_mem, mem_connectedComponent, true_and]
  intro B hB
  rw [← Ultrafilter.coe_le_coe]
  intro s hs
  rw [connectedComponent_eq_iInter_isClopen, Set.mem_iInter] at hB
  let Z := { F : Ultrafilter α | s ∈ F }
  have hZ : IsClopen Z := ⟨ultrafilter_isClosed_basic s, ultrafilter_isOpen_basic s⟩
  exact hB ⟨Z, hZ, hs⟩

Goal state after:
Module: Mathlib.Data.List.Triplewise

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
p : α → α → α → Prop
⊢ Triplewise p (l₁ ++ l₂) ↔
    Triplewise p l₁ ∧
      Triplewise p l₂ ∧ (∀ (a : α), a ∈ l₁ → Pairwise (p a) l₂) ∧ ∀ (a : α), a ∈ l₂ → Pairwise (fun x y ↦ p x y a) l₁

Tactic:
by
  induction l₁ with grind [pairwise_cons]

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

Goal state before:
pp: ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n + 1
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
this✝ : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' | x' ≠ x}
t' : ↑ι' → Finset α := fun x' ↦ (t ↑x').erase y
⊢ Fintype.card ι - 1 = n

Tactic:
by rw [hn, Nat.add_succ_sub_one, add_zero]

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

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
p : P
l : List P
⊢ List.Sbtw R (p :: l) ↔ Pairwise (Sbtw R p) l ∧ List.Sbtw R l ∧ l ≠ [p]

Tactic:
sbtw_iff_triplewise_and_ne_pair,

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
p : P
l : List P
⊢ (Triplewise (Sbtw R) (p :: l) ∧ ∀ (a : P), p :: l ≠ [a, a]) ↔ Pairwise (Sbtw R p) l ∧ List.Sbtw R l ∧ l ≠ [p]
Module: Mathlib.Analysis.Convex.BetweenList

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
p : P
l : List P
hp : Pairwise (Sbtw R p) l
hne : ¬l = [p]
⊢ Triplewise (Sbtw R) l ↔ List.Sbtw R l

Tactic:
sbtw_iff_triplewise_and_ne_pair,

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
p : P
l : List P
hp : Pairwise (Sbtw R p) l
hne : ¬l = [p]
⊢ Triplewise (Sbtw R) l ↔ Triplewise (Sbtw R) l ∧ ∀ (a : P), l ≠ [a, a]
Module: Mathlib.Combinatorics.Hall.Finite

Goal state before:
pp: case refine_1
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n + 1
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
this✝ : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' | x' ≠ x}
t' : ↑ι' → Finset α := fun x' ↦ (t ↑x').erase y
card_ι' : Fintype.card ↑ι' = n
f' : ↑ι' → α
hfinj : Function.Injective f'
hfr : ∀ (x : ↑ι'), f' x ∈ t' x
z₁ z₂ : ι
⊢ (fun z ↦ if h : z = x then y else f' ⟨z, h⟩) z₁ = (fun z ↦ if h : z = x then y else f' ⟨z, h⟩) z₂ → z₁ = z₂

Tactic:
have key : ∀ {x}, y ≠ f' x := by
      intro x h
      simpa [t', ← h] using hfr x

Goal state after:
case refine_1
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n + 1
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
this✝ : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' | x' ≠ x}
t' : ↑ι' → Finset α := fun x' ↦ (t ↑x').erase y
card_ι' : Fintype.card ↑ι' = n
f' : ↑ι' → α
hfinj : Function.Injective f'
hfr : ∀ (x : ↑ι'), f' x ∈ t' x
z₁ z₂ : ι
key : ∀ {x : ↑ι'}, y ≠ f' x
⊢ (fun z ↦ if h : z = x then y else f' ⟨z, h⟩) z₁ = (fun z ↦ if h : z = x then y else f' ⟨z, h⟩) z₂ → z₁ = z₂
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: case mp.inr
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
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : z = x
⊢ x = (lineMap x z) ty

Tactic:
h,

Goal state after:
case mp.inr
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
x z : P
ty : R
hty : ty ∈ Set.Icc 0 1
tx : R
htx : tx ∈ Set.Icc 0 1
h : z = x
⊢ x = (lineMap x x) ty
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: case a
J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j k : J
f : i ⟶ j
g : j ⟶ k
h : F.eventualRange k = range ⇑(ConcreteCategory.hom (F.map g))
⊢ range ⇑(ConcreteCategory.hom (F.map (f ≫ g))) ⊆ F.eventualRange k

Tactic:
h,

Goal state after:
case a
J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j k : J
f : i ⟶ j
g : j ⟶ k
h : F.eventualRange k = range ⇑(ConcreteCategory.hom (F.map g))
⊢ range ⇑(ConcreteCategory.hom (F.map (f ≫ g))) ⊆ range ⇑(ConcreteCategory.hom (F.map g))
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j k : J
s : Set (F.obj i)
X✝ Y✝ : J
g : X✝ ⟶ Y✝
x : (fun X ↦ X) (F.obj X✝)
h : ∀ (i_1 : X✝ ⟶ i), x ∈ ⇑(ConcreteCategory.hom (F.map i_1)) ⁻¹' s
f : Y✝ ⟶ i
⊢ (ConcreteCategory.hom (F.map g)) x ∈ ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' s

Tactic:
rw [← mem_preimage, preimage_preimage, mem_preimage]

Goal state after:
J : Type u
inst✝ : Category.{v_1, u} J
F : J ⥤ Type v
i j k : J
s : Set (F.obj i)
X✝ Y✝ : J
g : X✝ ⟶ Y✝
x : (fun X ↦ X) (F.obj X✝)
h : ∀ (i_1 : X✝ ⟶ i), x ∈ ⇑(ConcreteCategory.hom (F.map i_1)) ⁻¹' s
f : Y✝ ⟶ i
⊢ (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (F.map g)) x) ∈ s
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : j ⟶ i
x : (fun X ↦ X) (F.obj j)
hx : ∀ ⦃i : J⦄ (f : i ⟶ j), x ∈ range ⇑(ConcreteCategory.hom (F.map f))
⊢ ∀ ⦃i_1 : J⦄ (f_1 : i_1 ⟶ i), (ConcreteCategory.hom (F.map f)) x ∈ range ⇑(ConcreteCategory.hom (F.map f_1))

Tactic:
intro k

Goal state after:
J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i j : J
inst✝ : IsCofilteredOrEmpty J
f : j ⟶ i
x : (fun X ↦ X) (F.obj j)
hx : ∀ ⦃i : J⦄ (f : i ⟶ j), x ∈ range ⇑(ConcreteCategory.hom (F.map f))
k : J
⊢ ∀ (f_1 : k ⟶ i), (ConcreteCategory.hom (F.map f)) x ∈ range ⇑(ConcreteCategory.hom (F.map f_1))
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: ι : Type u
α : Type v
t : ι → Finset α
ι' : Finset ι
⊢ Finite ↑(hallMatchingsOn t ι')

Tactic:
by
  classical
    rw [hallMatchingsOn]
    let g : hallMatchingsOn t ι' → ι' → ι'.biUnion t := by
      rintro f i
      refine ⟨f.val i, ?_⟩
      rw [mem_biUnion]
      exact ⟨i, i.property, f.property.2 i⟩
    apply Finite.of_injective g
    intro f f' h
    ext a
    rw [funext_iff] at h
    simpa [g] using h a

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

Goal state before:
pp: case mp
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
w : Fin (1 + 1) → R
hw : ∑ i, w i = 1
h01 : ∀ (i : Fin (1 + 1)), w i ∈ Set.Icc 0 1
h : w = Finset.affineCombinationLineMapWeights 0 1 (w 1)
⊢ (Finset.affineCombination R Finset.univ s.points) w ∈ affineSegment R (s.points 0) (s.points 1)

Tactic:
h,

Goal state after:
case mp
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
w : Fin (1 + 1) → R
hw : ∑ i, w i = 1
h01 : ∀ (i : Fin (1 + 1)), w i ∈ Set.Icc 0 1
h : w = Finset.affineCombinationLineMapWeights 0 1 (w 1)
⊢ (Finset.affineCombination R Finset.univ s.points) (Finset.affineCombinationLineMapWeights 0 1 (w 1)) ∈
    affineSegment R (s.points 0) (s.points 1)