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

Goal state before:
pp: case neg
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
s : Set X
S : ℕ → Set X := fun n ↦ {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ∞
⊢ ∑' (k : ℕ), μ (S (k + 1) \ S k) ≠ ∞

Tactic:
← tsum_even_add_odd ENNReal.summable ENNReal.summable,

Goal state after:
case neg
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
s : Set X
S : ℕ → Set X := fun n ↦ {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ∞
⊢ ∑' (k : ℕ), μ (S (2 * k + 1) \ S (2 * k)) + ∑' (k : ℕ), μ (S (2 * k + 1 + 1) \ S (2 * k + 1)) ≠ ∞
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : μH[↑d] s = ∞
⊢ ↑d ≤ ⨆ d, ⨆ (_ : μH[↑d] s = ∞), ↑d

Tactic:
exact le_iSup₂ (α := ℝ≥0∞) d h

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
h : f.ker = ⊥
g : U ≃ₗ[𝕜] ↥f.range := LinearEquiv.ofBijective f.rangeRestrict ⋯
⊢ ¬f.normDet = 0

Tactic:
let bu := stdOrthonormalBasis 𝕜 U

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
h : f.ker = ⊥
g : U ≃ₗ[𝕜] ↥f.range := LinearEquiv.ofBijective f.rangeRestrict ⋯
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
⊢ ¬f.normDet = 0
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
hs : Nonempty ↥s
t : Set P
ht : MeasurableSet t
⊢ μHE[finrank ℝ V] t =
    ∫⁻ (x : ↥s), μHE[finrank ℝ ↥s.directionᗮ] (t ∩ ↑(mk' (↑x) s.directionᗮ)) ∂μHE[finrank ℝ ↥s.direction]

Tactic:
obtain p := hs.some
  rw [← (s.direction.measurePreserving_measurableEquivProd p.val).symm.measure_preimage_equiv,
    volume_eq_prod, prod_apply (by measurability), euclideanHausdorffMeasure_eq,
    MeasurableEmbedding.lintegral_map
        (by simpa using (IsometryEquiv.vaddConst p).toHomeomorph.measurableEmbedding)]
  congr with x
  let u : Set (mk' (x +ᵥ p).val s.directionᗮ) := Subtype.val ⁻¹' (t ∩ mk' (x +ᵥ p).val s.directionᗮ)
  have hu : MeasurableSet u :=
    (ht.inter (closed_of_finiteDimensional _).measurableSet).preimage measurable_subtype_coe
  have hinter : t ∩ (mk' (x +ᵥ p).val s.directionᗮ) = Subtype.val '' u := by
    ext x
    simp [u]
  have hxp : (x +ᵥ p).val ∈ mk' (x +ᵥ p).val s.directionᗮ := by simp
  have hrank : finrank ℝ s.directionᗮ = finrank ℝ (mk' (x +ᵥ p).val s.directionᗮ).direction := by
    rw [direction_mk']
  rw [IsometryEquiv.vaddConst_apply, hinter, euclideanHausdorffMeasure_coe_image, hrank,
    euclideanHausdorffMeasure_eq ⟨x +ᵥ p, hxp⟩, map_apply (by fun_prop) hu]
  /- we have ⊢ volume (a : Set A) = volume (b : Set B). We'd like show a = b, but A and B are
    non-defeq subspaces!
    Lucky we have just developed euclideanHausdorffMeasure, which allows us to move the measure to
    the global vector space. -/
  simp_rw [← InnerProductSpace.euclideanHausdorffMeasure_eq_volume]
  conv_lhs => rw [← isometry_subtype_coe.euclideanHausdorffMeasure_image]
  conv_rhs => rw [← isometry_subtype_coe.euclideanHausdorffMeasure_image]
  congrm μHE[$hrank] ?_
  ext y
  simp [u, vadd_vadd, add_comm]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
⊢ μHE[finrank ℝ V] t = ‖v‖ₑ * ∫⁻ (x : ℝ), μHE[finrank ℝ V - 1] (t ∩ ↑(AffineSubspace.mk' (x • v +ᵥ p) (ℝ ∙ v)ᗮ))

Tactic:
have hrank : finrank ℝ (AffineSubspace.mk' p (ℝ ∙ v)).direction = 1 := by
    rw [AffineSubspace.direction_mk']
    apply finrank_span_singleton hv

Goal state after:
V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
hrank : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction = 1
⊢ μHE[finrank ℝ V] t = ‖v‖ₑ * ∫⁻ (x : ℝ), μHE[finrank ℝ V - 1] (t ∩ ↑(AffineSubspace.mk' (x • v +ᵥ p) (ℝ ∙ v)ᗮ))
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup U
inst✝⁴ : InnerProductSpace 𝕜 U
inst✝³ : FiniteDimensional 𝕜 U
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : CompleteSpace V
f : U →L[𝕜] V
this✝ : CompleteSpace U
this : CompleteSpace ↥(↑f).range
⊢ ↑((↑f).normDet ^ 2) = (ContinuousLinearMap.adjoint f ∘SL f).det

Tactic:
let bu := stdOrthonormalBasis 𝕜 U

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup U
inst✝⁴ : InnerProductSpace 𝕜 U
inst✝³ : FiniteDimensional 𝕜 U
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace 𝕜 V
inst✝ : CompleteSpace V
f : U →L[𝕜] V
this✝ : CompleteSpace U
this : CompleteSpace ↥(↑f).range
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
⊢ ↑((↑f).normDet ^ 2) = (ContinuousLinearMap.adjoint f ∘SL f).det
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x y : E
h : x ≠ y
⊢ dimH (segment ℝ x y) = 1

Tactic:
by
  rw [Convex.dimH_eq_finrank_vectorSpan (convex_segment x y) ⟨x, left_mem_segment ℝ x y⟩,
      vectorSpan_segment]
  simp [finrank_span_singleton (sub_ne_zero.mpr h.symm)]

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

Goal state before:
pp: X : Type u_2
inst✝³ : EMetricSpace X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst✝ : ∀ (n : β), Countable (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
ε : ℝ≥0∞
hε : 0 < ε
c : ℝ≥0∞
hc : liminf (fun n ↦ ∑' (i : ι n), m (ediam (t n i))) l < c
n : β
hn : ∑' (i : ι n), m (ediam (t n i)) < c
hrn : r n < ε
htn : ∀ (i : ι n), ediam (t n i) ≤ r n
hstn : s ⊆ ⋃ i, t n i
u : ℕ → Set X := fun j ↦ ⋃ b ∈ decode₂ (ι n) j, t n b
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)) ≤ c

Tactic:
refine iInf₂_le_of_le u (by rwa [iUnion_decode₂]) ?_

Goal state after:
X : Type u_2
inst✝³ : EMetricSpace X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst✝ : ∀ (n : β), Countable (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
ε : ℝ≥0∞
hε : 0 < ε
c : ℝ≥0∞
hc : liminf (fun n ↦ ∑' (i : ι n), m (ediam (t n i))) l < c
n : β
hn : ∑' (i : ι n), m (ediam (t n i)) < c
hrn : r n < ε
htn : ∀ (i : ι n), ediam (t n i) ≤ r n
hstn : s ⊆ ⋃ i, t n i
u : ℕ → Set X := fun j ↦ ⋃ b ∈ decode₂ (ι n) j, t n b
⊢ ⨅ (_ : ∀ (n : ℕ), ediam (u n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (u n).Nonempty), m (ediam (u n)) ≤ c
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H : μH[d₂] s ≠ 0 ∧ μH[d₁] s ≠ ∞
c : ℝ≥0
hc : c ≠ 0
this : 0 < ↑c ^ (d₂ - d₁)⁻¹
r : ℝ≥0
hr₀ : 0 ≤ ↑r
hrc : ↑r < ↑c ^ (d₂ - d₁)⁻¹
⊢ ↑r ^ d₂ ≤ ↑c * ↑r ^ d₁

Tactic:
← ENNReal.div_le_iff_le_mul (Or.inr ENNReal.coe_ne_top) (Or.inr <| mt ENNReal.coe_eq_zero.1 hc)

Goal state after:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H : μH[d₂] s ≠ 0 ∧ μH[d₁] s ≠ ∞
c : ℝ≥0
hc : c ≠ 0
this : 0 < ↑c ^ (d₂ - d₁)⁻¹
r : ℝ≥0
hr₀ : 0 ≤ ↑r
hrc : ↑r < ↑c ^ (d₂ - d₁)⁻¹
⊢ ↑r ^ d₂ / ↑r ^ d₁ ≤ ↑c
Module: Mathlib.Analysis.InnerProductSpace.Reproducing

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : RKHS 𝕜 H X V
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace V
⊢ (span 𝕜 {x | ∃ x_1 v, (kerFun H x_1) v = x}).topologicalClosure = ⊤

Tactic:
refine (orthogonal_eq_bot_iff.mp ((Submodule.eq_bot_iff _).mpr fun f fin ↦ DFunLike.ext f 0 ?_))

Goal state after:
𝕜 : Type u_1
inst✝⁷ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : RKHS 𝕜 H X V
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace V
f : H
fin : f ∈ (span 𝕜 {x | ∃ x_1 v, (kerFun H x_1) v = x}).topologicalClosureᗮ
⊢ ∀ (x : X), f x = 0 x
Module: Mathlib.Analysis.InnerProductSpace.StarOrder

Goal state before:
pp: 𝕜 : Type u_1
H : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : CompleteSpace H
inst✝¹ : Algebra ℝ (H →L[𝕜] H)
inst✝ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
f : H →L[𝕜] H
hf : f.IsPositive
c : ℝ
hc : c ∈ spectrum ℝ f
⊢ 0 ≤ c

Tactic:
contrapose! hc

Goal state after:
𝕜 : Type u_1
H : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : CompleteSpace H
inst✝¹ : Algebra ℝ (H →L[𝕜] H)
inst✝ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
f : H →L[𝕜] H
hf : f.IsPositive
c : ℝ
hc : c < 0
⊢ c ∉ spectrum ℝ f
Module: Mathlib.Analysis.InnerProductSpace.Reproducing

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : RKHS 𝕜 H X V
inst✝² : CompleteSpace H
inst✝¹ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
inst✝ : Fact K.PosSemidef
f g : H₀ K
⊢ (starRingEnd 𝕜)
      (Finsupp.sum f fun x' v' ↦
        Finsupp.sum g fun x v ↦
          match x' with
          | (x_1, v_1) => star v * v' * ⟪(K x_1 x.1) x.2, v_1⟫_𝕜) =
    Finsupp.sum f fun x z ↦
      match x with
      | (y, u) =>
        Finsupp.sum g fun x w ↦
          match x with
          | (x, v) => star z * w * ⟪(K x y) u, v⟫_𝕜

Tactic:
simp only [map_finsuppSum]

Goal state after:
𝕜 : Type u_1
inst✝⁸ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : RKHS 𝕜 H X V
inst✝² : CompleteSpace H
inst✝¹ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
inst✝ : Fact K.PosSemidef
f g : H₀ K
⊢ (Finsupp.sum f fun a b ↦ Finsupp.sum g fun a_1 b_1 ↦ (starRingEnd 𝕜) (star b_1 * b * ⟪(K a.1 a_1.1) a_1.2, a.2⟫_𝕜)) =
    Finsupp.sum f fun x z ↦ Finsupp.sum g fun x_1 w ↦ star z * w * ⟪(K x_1.1 x.1) x.2, x_1.2⟫_𝕜
Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : NormedField 𝕜'
inst✝² : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : FirstCountableTopology E
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i ↦ b i
bE' : (𝓝 0).HasBasis (fun x ↦ True) fun n ↦ c ^ n • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (i : ℕ), u i ∈ c ^ i • b i
hu' : ∀ (i : ℕ), f (u i) ∉ V
n : ℕ
⊢ (c ^ n)⁻¹ • u n ∈ b n

Tactic:
simpa only [Set.mem_smul_set_iff_inv_smul_mem₀ (pow_ne_zero n c_ne)] using hu n

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

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
hs : MeasurableSet s
⊢ (Measure.map ⇑(AffineMap.homothety x c) μH[d]) s = (‖c‖₊⁻¹ ^ d • μH[d]) s

Tactic:
rw [Measure.map_apply (AffineMap.homothety_continuous x c).measurable hs,
    hausdorffMeasure_homothety_preimage hd x hc s, Measure.smul_apply]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ⟪x, o.rightAngleRotation y⟫ = -(o.areaForm x) y

Tactic:
by
  rw [rightAngleRotation]
  exact o.inner_rightAngleRotationAux₁_right x y

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WeakSpace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
he₁ : ∀ (f : StrongDual 𝕜 F), Continuous ⇑(e.dualMap ↑f)
he₂ : ∀ (f : StrongDual 𝕜 E), Continuous ⇑(e.symm.dualMap ↑f)
⊢ ⇑e '' closure s = closure (⇑e '' s)

Tactic:
refine le_antisymm ((e : E →ₗ[𝕜] F).image_closure_of_convex hs he₁) ?_
  simp only [← Set.image_subset_image_iff e.symm.injective]
  simpa [Set.image_image]
    using (e.symm : F →ₗ[𝕜] E).image_closure_of_convex (hs.linear_image (e : E →ₗ[𝕜] F)) he₂

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

Goal state before:
pp: z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
⊢ ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n =
    ↑n / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1)

Tactic:
by
  have der1 :
    ∀ x : ℝ,
      x ∈ uIcc 0 (π / 2) →
        HasDerivAt (fun y : ℝ => (cos y : ℂ) ^ n) (-n * sin x * (cos x : ℂ) ^ (n - 1)) x := by
    intro x _
    have b : HasDerivAt (fun y : ℝ => (cos y : ℂ)) (-sin x) x := by
      simpa using (hasDerivAt_cos x).ofReal_comp
    convert! HasDerivAt.comp x (hasDerivAt_pow _ _) b using 1
    ring
  convert! (config := { sameFun := true })
    integral_mul_deriv_eq_deriv_mul der1 (fun x _ => antideriv_cos_comp_const_mul hz x) _ _ using 2
  · ext1 x; rw [mul_comm]
  · rw [Complex.ofReal_zero, mul_zero, Complex.sin_zero, zero_div, mul_zero, sub_zero,
      cos_pi_div_two, Complex.ofReal_zero, zero_pow (by positivity : n ≠ 0), zero_mul, zero_sub,
      ← integral_neg, ← integral_const_mul]
    refine integral_congr fun x _ => ?_
    ring
  · apply Continuous.intervalIntegrable (by fun_prop)
  · apply Continuous.intervalIntegrable <| by fun_prop

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

Goal state before:
pp: z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
nne : ↑n ≠ 0
this :
  ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n =
    ↑n / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1)
⊢ (1 - 4 * z ^ 2 / ↑n ^ 2) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n =
    (↑n - 1) / ↑n * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2)

Tactic:
integral_sin_mul_sin_mul_cos_pow_eq hn hz,

Goal state after:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
nne : ↑n ≠ 0
this :
  ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n =
    ↑n / (2 * z) *
      ((↑n / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
        (↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2))
⊢ (1 - 4 * z ^ 2 / ↑n ^ 2) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n =
    (↑n - 1) / ↑n * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: u : ℂ
hu : 0 < u.re
⊢ -1 < (u - 1).re

Tactic:
rwa [sub_re, one_re, ← sub_pos, sub_neg_eq_add, sub_add_cancel]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case succ
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : ↑m < x - 1
hy' : x - 1 ≤ ↑m + 1
this :
  ∀ᶠ (n : ℕ) in atTop,
    logGammaSeq (x - 1) n = logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)
hm :
  Tendsto
    ((fun x_1 ↦ logGammaSeq x (x_1 - 1) + x * (log (↑(x_1 - 1) + 1) - log ↑(x_1 - 1)) - log (x - 1) + log (x - 1)) ∘
      fun a ↦ a + 1)
    atTop (𝓝 (f (x - 1) - f 1 + log (x - 1)))
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Tactic:
have :
      ((fun x_1 : ℕ =>
            (fun n : ℕ =>
                  logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1))
                x_1 +
              (fun b : ℕ => log (x - 1)) x_1) ∘
          fun a : ℕ => a + 1) =
        fun n => logGammaSeq x n + x * (log (↑n + 1) - log ↑n) := by
      ext1 n
      dsimp only [Function.comp_apply]
      rw [sub_add_cancel, Nat.add_sub_cancel]

Goal state after:
case succ
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : ↑m < x - 1
hy' : x - 1 ≤ ↑m + 1
this✝ :
  ∀ᶠ (n : ℕ) in atTop,
    logGammaSeq (x - 1) n = logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)
hm :
  Tendsto
    ((fun x_1 ↦ logGammaSeq x (x_1 - 1) + x * (log (↑(x_1 - 1) + 1) - log ↑(x_1 - 1)) - log (x - 1) + log (x - 1)) ∘
      fun a ↦ a + 1)
    atTop (𝓝 (f (x - 1) - f 1 + log (x - 1)))
this :
  ((fun x_1 ↦
        (fun n ↦ logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)) x_1 +
          (fun b ↦ log (x - 1)) x_1) ∘
      fun a ↦ a + 1) =
    fun n ↦ logGammaSeq x n + x * (log (↑n + 1) - log ↑n)
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : IsStrictOrderedRing k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
this : Tendsto (fun u ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)
t : k
u : V
ht : 0 < t
hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s
h : t • u +ᵥ c • v +ᵥ p ∈ s
⊢ SameRay k ((c • v +ᵥ p) -ᵥ (-(c • u) +ᵥ c • v +ᵥ p)) ((t • u +ᵥ c • v +ᵥ p) -ᵥ (c • v +ᵥ p))

Tactic:
vsub_vadd_eq_vsub_sub,

Goal state after:
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : IsStrictOrderedRing k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
this : Tendsto (fun u ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)
t : k
u : V
ht : 0 < t
hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s
h : t • u +ᵥ c • v +ᵥ p ∈ s
⊢ SameRay k ((c • v +ᵥ p) -ᵥ (c • v +ᵥ p) - -(c • u)) ((t • u +ᵥ c • v +ᵥ p) -ᵥ (c • v +ᵥ p))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
k : ℤ
⊢ (↑π * s).im ≠ (↑k * ↑π).im

Tactic:
rw [im_ofReal_mul, ← ofReal_intCast, ← ofReal_mul, ofReal_im]

Goal state after:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
k : ℤ
⊢ π * s.im ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
m : ℕ
hs : s = -↑m
⊢ s.re ≤ 0

Tactic:
simpa only [hs, neg_re, ← ofReal_natCast, ofReal_re, neg_nonpos] using Nat.cast_nonneg _

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: case zero
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormOneClass F
inst✝¹ : NormMulClass F
inst✝ : NormedAlgebra ℂ F
x : F
M : ℝ
hM : 0 ≤ M
h : ∀ (z' : ℂ), M ≤ ‖x - (algebraMap ℂ F) z'‖
c : ℂ
p : ℂ[X]
hp : p.IsMonicOfDegree 0
⊢ M ^ 0 ≤ ‖(aeval (x - (algebraMap ℂ F) c)) p‖

Tactic:
simp [isMonicOfDegree_zero_iff.mp hp]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential

Goal state before:
pp: q : ℍ
hq : q.re = 0
c s : ℝ
hc : HasSum (fun a ↦ ↑((-1) ^ a * ‖q‖ ^ (2 * a) / ↑(2 * a)!)) ↑c
hs : HasSum (fun z ↦ ((-1) ^ z * ‖q‖ ^ (2 * z + 1) / ↑(2 * z + 1)! / ‖q‖) • q) ((s / ‖q‖) • q)
n : ℕ
⊢ ((expSeries ℝ ℍ (2 * n)) fun x ↦ q) = ↑((-1) ^ n * ‖q‖ ^ (2 * n) / ↑(2 * n)!)

Tactic:
rw [expSeries_even_of_imaginary hq]

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
f g : RingSeminorm R
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
R : Type u_1
inst✝ : NonUnitalRing R
g : RingSeminorm R
toAddGroupSeminorm✝ : AddGroupSeminorm R
mul_le'✝ : ∀ (x y : R), toAddGroupSeminorm✝.toFun (x * y) ≤ toAddGroupSeminorm✝.toFun x * toAddGroupSeminorm✝.toFun y
h : (fun f ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝, mul_le' := mul_le'✝ } = (fun f ↦ f.toFun) g
⊢ { toAddGroupSeminorm := toAddGroupSeminorm✝, mul_le' := mul_le'✝ } = g
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f✝ f f' : AlgebraNorm R S
h : ⇑f.toRingSeminorm = ⇑f'.toRingSeminorm
⊢ f = f'

Tactic:
cases f

Goal state after:
case mk
R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f f' : AlgebraNorm R S
toRingNorm✝ : RingNorm S
smul'✝ : ∀ (a : R) (x : S), toRingNorm✝.toFun (a • x) = ‖a‖ * toRingNorm✝.toFun x
h : ⇑{ toRingNorm := toRingNorm✝, smul' := smul'✝ }.toRingSeminorm = ⇑f'.toRingSeminorm
⊢ { toRingNorm := toRingNorm✝, smul' := smul'✝ } = f'
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
f g : RingNorm R
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
R : Type u_1
inst✝ : NonUnitalRing R
g : RingNorm R
toRingSeminorm✝ : RingSeminorm R
eq_zero_of_map_eq_zero'✝ : ∀ (x : R), toRingSeminorm✝.toFun x = 0 → x = 0
h :
  (fun f ↦ f.toFun) { toRingSeminorm := toRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toRingSeminorm := toRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ } = g