mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: ι : Type u_1
A : ι → Type u_2
inst✝² : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝¹ : DecidableEq ι
p : ℝ
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : ↑(#s) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
⊢ T μ p f (insert i s) = ∫⋯∫⁻_insert i s, f ^ (1 - ↑(#s) * p) * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) ^ p ∂μ

Tactic:
simp_rw [T, card_insert_of_notMem hi]

Goal state after:
ι : Type u_1
A : ι → Type u_2
inst✝² : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝¹ : DecidableEq ι
p : ℝ
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : ↑(#s) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
⊢ ∫⋯∫⁻_insert i s, f ^ (1 - (↑(#s + 1) - 1) * p) * ∏ i ∈ insert i s, (∫⋯∫⁻_{i}, f ∂μ) ^ p ∂μ =
    ∫⋯∫⁻_insert i s, f ^ (1 - ↑(#s) * p) * ∏ i ∈ insert i s, (∫⋯∫⁻_{i}, f ∂μ) ^ p ∂μ
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsPositive
hT' : T ≠ 0
α : 𝕜
h : (α • T).IsPositive
x : E
hx : 0 < ⟪x, T x⟫
this : 0 ≤ α * ⟪x, T x⟫
⊢ 0 ≤ α

Tactic:
exact le_of_smul_le_smul_of_pos_right (by simpa) hx

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace 𝕜 F
f₁ f₂ : E →ₗ[𝕜] E
h₁ : (f₂ - f₁).IsPositive
h₂ : (f₁ - f₂).IsPositive
x : E
hba2 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
← neg_le_neg_iff,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace 𝕜 F
f₁ f₂ : E →ₗ[𝕜] E
h₁ : (f₂ - f₁).IsPositive
h₂ : (f₁ - f₂).IsPositive
x : E
hba2 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Dynamics.BirkhoffSum.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
f : α → α
φ : α → M
h : φ ∘ f = φ
n : ℕ
⊢ birkhoffSum f φ n = n • φ

Tactic:
funext x

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
f : α → α
φ : α → M
h : φ ∘ f = φ
n : ℕ
x : α
⊢ birkhoffSum f φ n x = (n • φ) x
Module: Mathlib.Dynamics.BirkhoffSum.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
f : α → α
φ : α → M
h : φ ∘ f = φ
n : ℕ
⊢ birkhoffSum f φ n = n • φ

Tactic:
by
  funext x
  suffices ∀ k, φ (f^[k] x) = φ x by simp [birkhoffSum, this]
  intro k
  exact congrFun (iterate_invariant h k) x

Goal state after:
Module: Mathlib.Dynamics.BirkhoffSum.Basic

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝ : AddCommGroup G
f : α → α
g : α → G
n : ℕ
x : α
⊢ birkhoffSum f g n (f x) - (birkhoffSum f g (n + 1) x - g (f^[n] x)) = g (f^[n] x) - g x

Tactic:
← sub_eq_iff_eq_add.2 (birkhoffSum_succ' f g n x),

Goal state after:
α : Type u_1
G : Type u_2
inst✝ : AddCommGroup G
f : α → α
g : α → G
n : ℕ
x : α
⊢ birkhoffSum f g n (f x) - (birkhoffSum f g (n + 1) x - g (f^[n] x)) =
    g (f^[n] x) - (birkhoffSum f g (n + 1) x - birkhoffSum f g n (f x))
Module: Mathlib.Dynamics.BirkhoffSum.Average

Goal state before:
pp: R : Type u_1
α : Type u_2
M : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : α → α
g : α → M
h : g ∘ f = g
n : ℕ
hn : ↑n ≠ 0
⊢ birkhoffAverage R f g n = g

Tactic:
funext x

Goal state after:
R : Type u_1
α : Type u_2
M : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : α → α
g : α → M
h : g ∘ f = g
n : ℕ
hn : ↑n ≠ 0
x : α
⊢ birkhoffAverage R f g n x = g x
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : E →L[𝕜] F
x : E ⊗[𝕜] G
n : ℕ
e : Fin n → E
g : Fin n → G
hx : x = ∑ j, e j ⊗ₜ[𝕜] g j
c : E ⊗[𝕜] G →₀ 𝕜
hc_supp : ↑c.support ⊆ {t | ∃ m n, m ⊗ₜ[𝕜] n = t}
hc : (c.sum fun mi r ↦ r • mi) = x
m : ℕ
A : Fin m → Fin n → 𝕜
hA :
  ∀ (i j : Fin n),
    ‖f‖ ^ 2 • inner 𝕜 (e i) (e j) - (∑ i, Matrix.vecMulVec (A i) (star (A i))) i j = inner 𝕜 (f (e i)) (f (e j))
⊢ 0 ≤ RCLike.re (∑ z, ∑ x, ∑ y, inner 𝕜 (g y) (g x) * (A z y * star (A z) x))

Tactic:
Pi.star_apply,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : E →L[𝕜] F
x : E ⊗[𝕜] G
n : ℕ
e : Fin n → E
g : Fin n → G
hx : x = ∑ j, e j ⊗ₜ[𝕜] g j
c : E ⊗[𝕜] G →₀ 𝕜
hc_supp : ↑c.support ⊆ {t | ∃ m n, m ⊗ₜ[𝕜] n = t}
hc : (c.sum fun mi r ↦ r • mi) = x
m : ℕ
A : Fin m → Fin n → 𝕜
hA :
  ∀ (i j : Fin n),
    ‖f‖ ^ 2 • inner 𝕜 (e i) (e j) - (∑ i, Matrix.vecMulVec (A i) (star (A i))) i j = inner 𝕜 (f (e i)) (f (e j))
⊢ 0 ≤ RCLike.re (∑ x, ∑ x_1, ∑ x_2, inner 𝕜 (g x_2) (g x_1) * (A x x_2 * star (A x x_1)))
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case e'_4.h
F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : FiniteDimensional ℝ F
u : E → F
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p q : ℝ≥0
hp : 1 ≤ p
h2p : p < ↑(finrank ℝ E)
hpq : ↑p⁻¹ - (↑(finrank ℝ E))⁻¹ ≤ (↑q)⁻¹
hs : Bornology.IsBounded s
hq0 : ¬q = 0
p' : ℝ≥0 := (p⁻¹ - (↑(finrank ℝ E))⁻¹)⁻¹
hp' : ↑p'⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹
this : ↑q ≤ ↑p'
t : ℝ≥0 := (μ s).toNNReal ^ (1 / ↑q - 1 / ↑p')
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ ↑p
⊢ 0 ≤ 1 / ↑q - 1 / ↑p'

Tactic:
rw [one_div, one_div]

Goal state after:
case e'_4.h
F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : FiniteDimensional ℝ F
u : E → F
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p q : ℝ≥0
hp : 1 ≤ p
h2p : p < ↑(finrank ℝ E)
hpq : ↑p⁻¹ - (↑(finrank ℝ E))⁻¹ ≤ (↑q)⁻¹
hs : Bornology.IsBounded s
hq0 : ¬q = 0
p' : ℝ≥0 := (p⁻¹ - (↑(finrank ℝ E))⁻¹)⁻¹
hp' : ↑p'⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹
this : ↑q ≤ ↑p'
t : ℝ≥0 := (μ s).toNNReal ^ (1 / ↑q - 1 / ↑p')
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ ↑p
⊢ 0 ≤ (↑q)⁻¹ - (↑p')⁻¹
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
hrank : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction = 1
hrank' : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ = finrank ℝ V - 1
f : ℝ ≃L[ℝ] ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction :=
  (ContinuousLinearEquiv.toSpanNonzeroSingleton ℝ v hv).trans
    (ContinuousLinearEquiv.ofEq (ℝ ∙ v) (AffineSubspace.mk' p (ℝ ∙ v)).direction ⋯)
hf : MeasurableEmbedding ⇑f
p' : ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⟨p, ⋯⟩
⊢ μHE[finrank ℝ V] t = ‖v‖ₑ * ∫⁻ (x : ℝ), μHE[finrank ℝ V - 1] (t ∩ ↑(AffineSubspace.mk' (x • v +ᵥ p) (ℝ ∙ v)ᗮ))

Tactic:
let g : ℝ → AffineSubspace.mk' p (ℝ ∙ v) := IsometryEquiv.vaddConst p' ∘ f

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
hrank' : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ = finrank ℝ V - 1
f : ℝ ≃L[ℝ] ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction :=
  (ContinuousLinearEquiv.toSpanNonzeroSingleton ℝ v hv).trans
    (ContinuousLinearEquiv.ofEq (ℝ ∙ v) (AffineSubspace.mk' p (ℝ ∙ v)).direction ⋯)
hf : MeasurableEmbedding ⇑f
p' : ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⟨p, ⋯⟩
g : ℝ → ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⇑(IsometryEquiv.vaddConst p') ∘ ⇑f
⊢ μHE[finrank ℝ V] t = ‖v‖ₑ * ∫⁻ (x : ℝ), μHE[finrank ℝ V - 1] (t ∩ ↑(AffineSubspace.mk' (x • v +ᵥ p) (ℝ ∙ v)ᗮ))
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
⊢ ⨆ r, ⨆ (_ : r > 0), boundedBy (extend fun s x ↦ ∞) = ⊤

Tactic:
extend_top,

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
⊢ ⨆ r, ⨆ (_ : r > 0), boundedBy ⊤ = ⊤
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
hrank : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction = 1
hrank' : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ = finrank ℝ V - 1
f : ℝ ≃L[ℝ] ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction :=
  (ContinuousLinearEquiv.toSpanNonzeroSingleton ℝ v hv).trans
    (ContinuousLinearEquiv.ofEq (ℝ ∙ v) (AffineSubspace.mk' p (ℝ ∙ v)).direction ⋯)
hf : MeasurableEmbedding ⇑f
p' : ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⟨p, ⋯⟩
g : ℝ → ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⇑(IsometryEquiv.vaddConst p') ∘ ⇑f
hadd : MeasurableEmbedding ⇑(IsometryEquiv.vaddConst p')
hg : MeasurableEmbedding g
hm : μHE[finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction] = ‖v‖ₑ • map g volume
hx : ∀ (x : ℝ), x • v +ᵥ p = ↑(g x)
⊢ μHE[finrank ℝ V] t = ‖v‖ₑ * ∫⁻ (x : ℝ), μHE[finrank ℝ V - 1] (t ∩ ↑(AffineSubspace.mk' (x • v +ᵥ p) (ℝ ∙ v)ᗮ))

Tactic:
simp_rw [(AffineSubspace.mk' p (ℝ ∙ v)).euclideanHausdorffMeasure_eq_lintegral ht, hx,
    hm, lintegral_smul_measure, hg.lintegral_map, smul_eq_mul, hrank', AffineSubspace.direction_mk']

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y : E
⊢ Continuous fun r ↦ (starRingEnd 𝕜) ↑r * inner_ 𝕜 x y

pp: case refine_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y : E
X : ℚ
⊢ ((fun r ↦ inner_ 𝕜 (↑r • x) y) ∘ Rat.cast) X = ((fun r ↦ (starRingEnd 𝕜) ↑r * inner_ 𝕜 x y) ∘ Rat.cast) X

Tactic:
· exact (continuous_conj.comp continuous_ofReal).mul continuous_const

Goal state after:
case refine_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y : E
X : ℚ
⊢ ((fun r ↦ inner_ 𝕜 (↑r • x) y) ∘ Rat.cast) X = ((fun r ↦ (starRingEnd 𝕜) ↑r * inner_ 𝕜 x y) ∘ Rat.cast) X
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
this : ∀ {r : 𝕜} (s : Set E), μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s
⊢ μH[d] s ≤ ↑(‖r‖₊⁻¹ ^ d) * μH[d] (r • s)

Tactic:
← nnnorm_inv

Goal state after:
𝕜 : Type u_4
E : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : 0 ≤ d
r : 𝕜
hr : r ≠ 0
s : Set E
this : ∀ {r : 𝕜} (s : Set E), μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s
⊢ μH[d] s ≤ ↑(‖r⁻¹‖₊ ^ d) * μH[d] (r • s)
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: ι : Type u_4
inst✝ : Fintype ι
s : ι → Set ℝ
⊢ (∀ (i : ι), ∃ i_1 i_2, ∃ (_ : i_1 < i_2), s i = Ioo ↑i_1 ↑i_2) → μH[↑(Fintype.card ι)] (univ.pi s) = ∏ x, volume (s x)

Tactic:
hs

Goal state after:
ι : Type u_4
inst✝ : Fintype ι
s : ι → Set ℝ
hs : ∀ (i : ι), ∃ i_1 i_2, ∃ (_ : i_1 < i_2), s i = Ioo ↑i_1 ↑i_2
⊢ μH[↑(Fintype.card ι)] (univ.pi s) = ∏ x, volume (s x)
Module: Mathlib.Analysis.LocallyConvex.Montel

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : IsTopologicalAddGroup E
inst✝⁷ : ContinuousSMul 𝕜₁ E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₂ F
inst✝¹ : T1Space E
inst✝ : MontelSpace 𝕜₁ E
s : Set (E →SL_c[σ] F)
⊢ IsOpen[UniformConvergenceCLM.instTopologicalSpace σ F {S | IsCompact S}] s →
    IsOpen[topologicalSpace] (⇑(LinearEquiv.toCompactConvergenceCLM σ E F) ⁻¹' s)

Tactic:
hs

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : IsTopologicalAddGroup E
inst✝⁷ : ContinuousSMul 𝕜₁ E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₂ F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₂ F
inst✝¹ : T1Space E
inst✝ : MontelSpace 𝕜₁ E
s : Set (E →SL_c[σ] F)
hs : IsOpen[UniformConvergenceCLM.instTopologicalSpace σ F {S | IsCompact S}] s
⊢ IsOpen[topologicalSpace] (⇑(LinearEquiv.toCompactConvergenceCLM σ E F) ⁻¹' s)
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: w z : ℂ
⊢ (Complex.orientation.kahler w) z = z * (starRingEnd ℂ) w

Tactic:
by
  rw [Orientation.kahler_apply_apply]
  apply Complex.ext <;> simp [mul_comm]

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

Goal state before:
pp: s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
this : ∀ (n : ℕ) (s : ℂ), -↑n < s.re → (∀ (m : ℕ), s ≠ -↑m) → DifferentiableAt ℂ Gamma s
⊢ -↑(⌊-s.re⌋₊ + 1) < s.re

Tactic:
by grind [Nat.lt_floor_add_one (-s.re)]

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

Goal state before:
pp: s✝ : ℂ
hs : ∀ (m : ℕ), s✝ ≠ -↑m
n : ℕ
s : ℂ
hsre : -↑n < s.re
⊢ (∀ (m : ℕ), s ≠ -↑m) → DifferentiableAt ℂ Gamma s

Tactic:
hs

Goal state after:
s✝ : ℂ
hs✝ : ∀ (m : ℕ), s✝ ≠ -↑m
n : ℕ
s : ℂ
hsre : -↑n < s.re
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ DifferentiableAt ℂ Gamma s
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_2.e'_4
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ x ∈ uIcc 0 (π / 2), HasDerivAt (fun y ↦ ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ (fun x ↦ Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) = fun x ↦ ↑(cos x) ^ n * Complex.cos (2 * z * ↑x)

Tactic:
ext1 x; rw [mul_comm]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 - z)⁻¹ - z‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2

Tactic:
by
  convert! norm_log_one_sub_inv_add_logTaylor_neg_le 1 hz using 2
  · simp [logTaylor_succ, logTaylor_zero, sub_eq_add_neg]
  · norm_num

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

Goal state before:
pp: u : ℂ
hu : u = 0
⊢ u.re ≤ 0

Tactic:
hu,

Goal state after:
u : ℂ
hu : u = 0
⊢ re 0 ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: u v : ℂ
hv : 0 < v.re
F : ℝ → ℂ := fun x ↦ ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ x ∈ Ioo 0 1, HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x ↦ u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = F 1 - F 0
hu : u = 0
⊢ u.re ≤ 0

Tactic:
hu,

Goal state after:
u v : ℂ
hv : 0 < v.re
F : ℝ → ℂ := fun x ↦ ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ x ∈ Ioo 0 1, HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x ↦ u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = F 1 - F 0
hu : u = 0
⊢ re 0 ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: f : ℝ → ℂ
hf : ContinuousOn f (Icc 0 (π / 2))
c_lt : ∀ y ∈ Icc 0 (π / 2), y ≠ 0 → cos y < cos 0
c_nonneg : ∀ x ∈ Icc 0 (π / 2), 0 ≤ cos x
c_zero_pos : 0 < cos 0
⊢ 0 ≤ π / 2

Tactic:
exact pi_div_two_pos.le

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

Goal state before:
pp: case succ.refine_2
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
this : u.betaIntegral (↑n.succ + 1) * u = ↑n.succ * (u + 1).betaIntegral ↑n.succ
hu : u = 0
⊢ u.re ≤ 0

Tactic:
hu,

Goal state after:
case succ.refine_2
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
this : u.betaIntegral (↑n.succ + 1) * u = ↑n.succ * (u + 1).betaIntegral ↑n.succ
hu : u = 0
⊢ re 0 ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: s : ℝ
⊢ s ∈ Ioi 0 → (log ∘ doublingGamma) s = (fun s ↦ log (Γ (s / 2)) + log (Γ (s / 2 + 1 / 2)) + s * log 2 - log (2 * √π)) s

Tactic:
hs

Goal state after:
s : ℝ
hs : s ∈ Ioi 0
⊢ (log ∘ doublingGamma) s = (fun s ↦ log (Γ (s / 2)) + log (Γ (s / 2 + 1 / 2)) + s * log 2 - log (2 * √π)) s
Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set P
⊢ s ∈ ⨆ v ∈ Metric.sphere 0 1, asymptoticNhds ℝ P v → s ∈ cobounded P

Tactic:
hs

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set P
hs : s ∈ ⨆ v ∈ Metric.sphere 0 1, asymptoticNhds ℝ P v
⊢ s ∈ cobounded P
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
⊢ asymptoticCone k Set.univ = Set.univ

Tactic:
rw [← AffineSubspace.top_coe k, asymptoticCone_affineSubspace Set.univ_nonempty,
    AffineSubspace.direction_top, Submodule.top_coe, closure_univ]

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

Goal state before:
pp: case hb
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this✝ : ↑n ^ z * ↑n ^ (1 - z) = ↑n
this : ∀ (j : ℕ), (z + ↑(j + 1)) * (1 - z + ↑j) = ↑((j + 1) ^ 2) * (1 - z ^ 2 / (↑j + 1) ^ 2)
⊢ ↑n ! ^ 2 ≠ 0

Tactic:
exact pow_ne_zero 2 (Nat.cast_ne_zero.mpr <| by positivity)

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.MazurUlam

Goal state before:
pp: E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
⊢ f.toRealAffineIsometryEquiv.toIsometryEquiv = f

Tactic:
ext
  rfl

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case «0».«1».«0».«0»
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
x✝ :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
hx : True
hy : (fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩
hxy :
  dist (t.points ((fun i ↦ i) ⟨0, ⋯⟩)) (t.points ((fun i ↦ i) ⟨1, ⋯⟩)) =
    dist (t.points ((fun i ↦ i) ⟨0, ⋯⟩)) (t.points ((fun i ↦ i) ⟨0, ⋯⟩))
⊢ (fun i ↦ i) ⟨0, ⋯⟩ = (fun i ↦ i) ⟨0, ⋯⟩ ∧ (fun i ↦ i) ⟨1, ⋯⟩ = (fun i ↦ i) ⟨0, ⋯⟩

Tactic:
simp +decide only at hy

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case «0».«1».«0».«1»
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
x✝ :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
hx : True
hy : (fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩
hxy :
  dist (t.points ((fun i ↦ i) ⟨0, ⋯⟩)) (t.points ((fun i ↦ i) ⟨1, ⋯⟩)) =
    dist (t.points ((fun i ↦ i) ⟨0, ⋯⟩)) (t.points ((fun i ↦ i) ⟨1, ⋯⟩))
⊢ (fun i ↦ i) ⟨0, ⋯⟩ = (fun i ↦ i) ⟨0, ⋯⟩ ∧ (fun i ↦ i) ⟨1, ⋯⟩ = (fun i ↦ i) ⟨1, ⋯⟩

Tactic:
simp +decide only at hy

Goal state after:
case «0».«1».«0».«1»
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
x✝ :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
hx : True
hxy :
  dist (t.points ((fun i ↦ i) ⟨0, ⋯⟩)) (t.points ((fun i ↦ i) ⟨1, ⋯⟩)) =
    dist (t.points ((fun i ↦ i) ⟨0, ⋯⟩)) (t.points ((fun i ↦ i) ⟨1, ⋯⟩))
hy : True
⊢ (fun i ↦ i) ⟨0, ⋯⟩ = (fun i ↦ i) ⟨0, ⋯⟩ ∧ (fun i ↦ i) ⟨1, ⋯⟩ = (fun i ↦ i) ⟨1, ⋯⟩