mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
⊢ χ.IsQuadratic ↔ χ ^ 2 = 1

Tactic:
refine ⟨fun h ↦ ext (fun x ↦ ?_), fun h x ↦ ?_⟩
  · rw [one_apply_coe, χ.pow_apply_coe]
    rcases h x with H | H | H
    · exact (not_isUnit_zero <| H ▸ IsUnit.map χ <| x.isUnit).elim
    · simp only [H, one_pow]
    · simp only [H, even_two, Even.neg_pow, one_pow]
  · by_cases hx : IsUnit x
    · refine .inr <| sq_eq_one_iff.mp ?_
      rw [← χ.pow_apply' two_ne_zero, h, MulChar.one_apply hx]
    · exact .inl <| map_nonunit χ hx

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: case intro
M : Type u_1
inst✝² : CommMonoid M
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : Finite Mˣ
χ : MulChar M R
val✝ : Fintype Mˣ
⊢ IsOfFinOrder χ

Tactic:
exact isOfFinOrder_iff_pow_eq_one.2 ⟨_, Fintype.card_pos, χ.pow_card_eq_one⟩

Goal state after:
Module: Mathlib.Analysis.Hofer

Goal state before:
pp: X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / 2 ^ k * ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x'
this : Nonempty X
F : ℕ → X → X
hF : ∀ (k : ℕ) (x' : X), d x' x ≤ 2 * ε ∧ 2 ^ k * ϕ x ≤ ϕ x' → d x' (F k x') ≤ ε / 2 ^ k ∧ 2 * ϕ x' < ϕ (F k x')
u : ℕ → X := fun n ↦ Nat.recOn n x F
hu :
  ∀ (n : ℕ), d (u n) x ≤ 2 * ε ∧ 2 ^ n * ϕ x ≤ ϕ (u n) → d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
n : ℕ
IH : ∀ m ≤ n, d (u m) (u (m + 1)) ≤ ε / 2 ^ m ∧ 2 * ϕ (u m) < ϕ (u (m + 1))
r : Finset ℕ := range (n + 1)
⊢ ∑ i ∈ r, ε / 2 ^ i = (∑ i ∈ r, (1 / 2) ^ i) * ε

Tactic:
by
            rw [Finset.sum_mul]
            simp
            field_simp

Goal state after:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case e'_4
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
p : ℝ
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ i ∈ insert i s

Tactic:
exact mem_insert_self i s

Goal state after:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case hbc
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
p : ℝ
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ ↑(#s) ≤ ↑#ι - 1

Tactic:
suffices (s.card : ℝ) + 1 ≤ #ι by linarith

Goal state after:
case hbc
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
p : ℝ
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ ↑(#s) + 1 ≤ ↑#ι
Module: Mathlib.Analysis.InnerProductSpace.LinearPMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
hT : Dense ↑T.domain
⊢ T†.IsClosed

Tactic:
rw [IsClosed, adjoint_graph_eq_graph_adjoint hT, Submodule.adjoint]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
hT : Dense ↑T.domain
⊢ _root_.IsClosed
    ↑(Submodule.map (↑(WithLp.linearEquiv 2 𝕜 (F × E)))
        (Submodule.map (↑((LinearEquiv.skewSwap 𝕜 F E).symm.trans (WithLp.linearEquiv 2 𝕜 (F × E)).symm)) T.graph)ᗮ)
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x x' : E
y y' : F
⊢ ‖x ⊗ₜ[𝕜] y - x' ⊗ₜ[𝕜] y'‖₊ ≤ ‖x‖₊ * ‖y‖₊ + ‖x'‖₊ * ‖y'‖₊

Tactic:
nnnorm_sub_le

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x x' : E
y y' : F
⊢ ‖x ⊗ₜ[𝕜] y‖₊ + ‖x' ⊗ₜ[𝕜] y'‖₊ ≤ ‖x‖₊ * ‖y‖₊ + ‖x'‖₊ * ‖y'‖₊
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
⊢ mapL 0 f = 0

Tactic:
by simp [mapL]

Goal state after:
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
⊢ mapL f 0 = 0

Tactic:
by simp [mapL]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
G : Type u_4
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
⊢ mapL (ContinuousLinearMap.id 𝕜 E) (ContinuousLinearMap.id 𝕜 G) = ContinuousLinearMap.id 𝕜 (E ⊗[𝕜] G)

Tactic:
by simp [mapL]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
f : E →L[𝕜] F
⊢ ContinuousLinearMap.rTensor G f = mapL f (ContinuousLinearMap.id 𝕜 G)

Tactic:
by simp [mapL]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
G : Type u_4
H : Type u_5
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
g : G →L[𝕜] H
⊢ ContinuousLinearMap.lTensor E g = mapL (ContinuousLinearMap.id 𝕜 E) g

Tactic:
by simp [mapL]

Goal state after:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: 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 : ℝ≥0
hp : 1 ≤ p
h2p : p < ↑(finrank ℝ E)
hs : Bornology.IsBounded s
⊢ eLpNorm u (↑p) μ ≤ ↑(eLpNormLESNormFDerivOfLeConst F μ s p p) * eLpNorm (fderiv ℝ u) (↑p) μ

Tactic:
refine eLpNorm_le_eLpNorm_fderiv_of_le μ hu h2u hp h2p ?_ hs

Goal state after:
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 : ℝ≥0
hp : 1 ≤ p
h2p : p < ↑(finrank ℝ E)
hs : Bornology.IsBounded s
⊢ ↑p⁻¹ - (↑(finrank ℝ E))⁻¹ ≤ (↑p)⁻¹
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: 𝕜 : Type u_3
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℕ
r : 𝕜
hr : r ≠ 0
s : Set E
⊢ μHE[d] (r • s) = ‖r‖₊ ^ d • μHE[d] s

Tactic:
rw [euclideanHausdorffMeasure_def, Measure.smul_apply, hausdorffMeasure_smul₀ (by simp) hr,
    Measure.smul_apply, smul_comm]
  simp

Goal state after:
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: case inr
ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
this : μH[↑(Fintype.card ι)] (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι)
⊢ dimH (Metric.ball x r) = ↑↑(Fintype.card ι)

Tactic:
refine dimH_of_hausdorffMeasure_ne_zero_ne_top ?_ ?_

Goal state after:
case inr.refine_1
ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
this : μH[↑(Fintype.card ι)] (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι)
⊢ μH[↑↑(Fintype.card ι)] (Metric.ball x r) ≠ 0

case inr.refine_2
ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
this : μH[↑(Fintype.card ι)] (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι)
⊢ μH[↑↑(Fintype.card ι)] (Metric.ball x r) ≠ ∞
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: case pos
𝕜 : 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
c : 𝕜
hc : ¬c = 0
h : f.ker = ⊥
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
bv' : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥(c • f).range := bv.map (LinearIsometryEquiv.ofEq f.range (c • f).range ⋯)
this : finrank 𝕜 U = Fintype.card (Fin (finrank 𝕜 U))
⊢ ‖((toMatrix bu.toBasis bv'.toBasis) (c • f).rangeRestrict).det‖ =
    ‖c ^ finrank 𝕜 U * ((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖

Tactic:
conv in c ^ finrank 𝕜 U => rw [this]

Goal state after:
case pos
𝕜 : 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
c : 𝕜
hc : ¬c = 0
h : f.ker = ⊥
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
bv' : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥(c • f).range := bv.map (LinearIsometryEquiv.ofEq f.range (c • f).range ⋯)
this : finrank 𝕜 U = Fintype.card (Fin (finrank 𝕜 U))
⊢ ‖((toMatrix bu.toBasis bv'.toBasis) (c • f).rangeRestrict).det‖ =
    ‖c ^ Fintype.card (Fin (finrank 𝕜 U)) * ((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖
Module: Mathlib.Analysis.InnerProductSpace.OfNorm

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
x y : E
hI' : I * I = -1
h₁ : ‖-x - y‖ = ‖x + y‖
⊢ ‖-x + y‖ = ‖x - y‖

Tactic:
rw [← neg_sub, norm_neg, sub_eq_neg_add]

Goal state after:
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
x : X
x✝¹ : 𝕜
x✝ : V
⊢ ↑(Finsupp.single (x, x✝¹ • x✝) 1) = (RingHom.id 𝕜) x✝¹ • ↑(Finsupp.single (x, x✝) 1)

Tactic:
by
    refine UniformSpace.Completion.denseRange_coe.eq_of_inner_left 𝕜 fun f ↦ ?_
    simp [inner_smul_left, inner_H₀_def, Finsupp.mul_sum, ← mul_assoc, mul_comm]

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

Goal state before:
pp: ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := fun n ↦ (i : ι) → Fin ⌈(↑(b i) - ↑(a i)) * ↑n⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) := fun n f ↦ univ.pi fun i ↦ Icc (↑(a i) + ↑↑(f i) / ↑n) (↑(a i) + (↑↑(f i) + 1) / ↑n)
A : Tendsto (fun n ↦ 1 / ↑n) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ 1 / ↑n
n : ℕ
hn : 1 ≤ n
npos : 0 < ↑n
x : ι → ℝ
hx : ∀ (i : ι), ↑(a i) < x i ∧ x i < ↑(b i)
f : γ n := fun i ↦ ⟨⌊(x i - ↑(a i)) * ↑n⌋₊, ⋯⟩
i : ι
⊢ ↑(a i) + ↑⌊(x i - ↑(a i)) * ↑n⌋₊ / ↑n ≤ ↑(a i) + (x i - ↑(a i)) * ↑n / ↑n

Tactic:
gcongr
          exact Nat.floor_le (mul_nonneg (sub_nonneg.2 (hx i).1.le) npos.le)

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
h : ⟪x, y⟫ = 0
⊢ |o.volumeForm ![x, y]| = ‖x‖ * ‖y‖

Tactic:
o.abs_volumeForm_apply_of_pairwise_orthogonal

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
h : ⟪x, y⟫ = 0
⊢ ∏ i, ‖![x, y] i‖ = ‖x‖ * ‖y‖

E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
h : ⟪x, y⟫ = 0
⊢ Pairwise fun i j ↦ ⟪![x, y] i, ![x, y] j⟫ = 0
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 : E
K : Submodule ℝ E := ℝ ∙ x
this : Nontrivial ↥Kᗮ
w : ↥Kᗮ
hw₀ : w ≠ 0
hw' : ⟪x, ↑w⟫ = 0
hw : ↑w ≠ 0
⊢ 0 < ‖↑w‖

Tactic:
norm_pos_iff

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
this : Nontrivial ↥Kᗮ
w : ↥Kᗮ
hw₀ : w ≠ 0
hw' : ⟪x, ↑w⟫ = 0
hw : ↑w ≠ 0
⊢ ↑w ≠ 0
Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

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✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜₂ F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜₂ F
x : E
y : F⋆
⊢ Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun A ↦ y (A x)

Tactic:
refine (continuous_pi_iff.mp continuous_inducingFn) ⟨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' : Continuous fun x ↦ (toWeakSpace 𝕜 F) (e ((toWeakSpace 𝕜 E).symm x))
h_convex : Convex ℝ (⇑e '' s)
⊢ ⇑e '' closure s ⊆ closure (⇑e '' s)

Tactic:
rw [← Set.image_subset_image_iff (toWeakSpace 𝕜 F).injective, h_convex.toWeakSpace_closure 𝕜]

Goal state after:
𝕜 : 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' : Continuous fun x ↦ (toWeakSpace 𝕜 F) (e ((toWeakSpace 𝕜 E).symm x))
h_convex : Convex ℝ (⇑e '' s)
⊢ ⇑(toWeakSpace 𝕜 F) '' ⇑e '' closure s ⊆ closure (⇑(toWeakSpace 𝕜 F) '' ⇑e '' s)
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
R : Type u_4
V : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : T2Space R
inst✝⁵ : ContinuousAdd R
inst✝⁴ : ContinuousConstSMul R R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : TopologicalSpace V
inst✝ : SeparatingDual R V
x✝¹ x✝ : V
h : (topDualPairing R V).flip x✝¹ = (topDualPairing R V).flip x✝
⊢ x✝¹ = x✝

Tactic:
by_contra hne
    obtain ⟨f, hf⟩ := SeparatingDual.exists_separating_of_ne (R := R) hne
    exact hf (DFunLike.congr_fun h f)

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
⊢ mellin (fun t ↦ f (t * a)) s = ↑a ^ (-s) • mellin f s

Tactic:
simpa only [mul_comm] using mellin_comp_mul_left f s ha

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

Goal state before:
pp: z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
c : HasDerivAt ((fun x ↦ x ^ (n - 1)) ∘ Complex.cos) (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x) ↑x
⊢ ↑(n - 1) = ↑n - 1

Tactic:
rw [Nat.cast_sub (one_le_two.trans hn), Nat.cast_one]

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

Goal state before:
pp: s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp : ∀ {c u : ℝ}, 0 < c → 0 < u → MemLp (f c u) (ENNReal.ofReal (1 / c)) (volume.restrict (Ioi 0))
x : ℝ
hx : x ∈ Ioi 0
⊢ 0 < a

Tactic:
by assumption

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

Goal state before:
pp: s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
f_mem_Lp : ∀ {c u : ℝ}, 0 < c → 0 < u → MemLp (f c u) (ENNReal.ofReal (1 / c)) (volume.restrict (Ioi 0))
x : ℝ
hx : x ∈ Ioi 0
⊢ 0 < b

Tactic:
by assumption

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

Goal state before:
pp: case hx
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ Γ x ^ a ≠ 0

pp: case hy
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ Γ y ^ (1 - a) ≠ 0

pp: case hx
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ 0 < Γ y

pp: case hx
x y a : ℝ
ha : 0 < a
hb : 0 < 1 - a
hab : a + (1 - a) = 1
hx : 0 < x
hy : 0 < y
⊢ 0 < Γ x

Tactic:
all_goals positivity

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

Goal state before:
pp: case succ
f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
n : ℕ
hn : f (x + ↑n) = f x + ∑ m ∈ Finset.range n, log (x + ↑m)
⊢ f (x + ↑(n + 1)) = f x + ∑ m ∈ Finset.range (n + 1), log (x + ↑m)

Tactic:
have : x + n.succ = x + n + 1 := by push_cast; ring
    rw [this, hf_feq, hn]
    · rw [Finset.range_add_one, Finset.sum_insert Finset.notMem_range_self]
      abel
    · linarith [(Nat.cast_nonneg n : 0 ≤ (n : ℝ))]

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

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
n : ℕ
⊢ f (x + ↑n) = f x + ∑ m ∈ Finset.range n, log (x + ↑m)

Tactic:
induction n with
  | zero => simp
  | succ n hn =>
    have : x + n.succ = x + n + 1 := by push_cast; ring
    rw [this, hf_feq, hn]
    · rw [Finset.range_add_one, Finset.sum_insert Finset.notMem_range_self]
      abel
    · linarith [(Nat.cast_nonneg n : 0 ≤ (n : ℝ))]

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
hs_bot : b < s.re
F : ℂ → ℝ → E := fun z t ↦ ↑t ^ (z - 1) • f t
F' : ℂ → ℝ → E := fun z t ↦ (↑t ^ (z - 1) * ↑(log t)) • f t
v : ℝ
hv0 : 0 < v
hv1 : v < s.re - b
hv2 : v < a - s.re
bound : ℝ → ℝ := fun t ↦ (t ^ (s.re + v - 1) + t ^ (s.re - v - 1)) * |log t| * ‖f t‖
h1 : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) (volume.restrict (Ioi 0))
h2 : IntegrableOn (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (F' s) (volume.restrict (Ioi 0))
h4 : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
j : ℝ
hj : b < j
hj' : j < a
w : ℝ
hw1 : b < w
hw2 : w < j
w' : ℝ
hw1' : j < w'
hw2' : w' < a
⊢ LocallyIntegrableOn (fun t ↦ |log t| * ‖f t‖) (Ioi 0) volume

Tactic:
simp_rw [mul_comm]
        refine hfc.norm.mul_continuousOn ?_ isOpen_Ioi.isLocallyClosed
        refine Continuous.comp_continuousOn _root_.continuous_abs (continuousOn_log.mono ?_)
        exact subset_compl_singleton_iff.mpr self_notMem_Ioi

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

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
m : ℕ
⊢ ↑m < x → x ≤ ↑m + 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Tactic:
induction m generalizing x with

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

Goal state before:
pp: s : ℝ
hs : s ∈ Ioi 0
h1 : √π ≠ 0
h2 : Γ (s / 2) ≠ 0
h3 : Γ (s / 2 + 1 / 2) ≠ 0
h4 : 2 ^ (s - 1) ≠ 0
⊢ log (Γ (s / 2) * Γ (s / 2 + 1 / 2) * 2 ^ (s - 1)) - log √π =
    (fun s ↦ log (Γ (s / 2)) + log (Γ (s / 2 + 1 / 2)) + s * log 2 - log (2 * √π)) s

Tactic:
log_mul (mul_ne_zero h2 h3) h4,

Goal state after:
s : ℝ
hs : s ∈ Ioi 0
h1 : √π ≠ 0
h2 : Γ (s / 2) ≠ 0
h3 : Γ (s / 2 + 1 / 2) ≠ 0
h4 : 2 ^ (s - 1) ≠ 0
⊢ log (Γ (s / 2) * Γ (s / 2 + 1 / 2)) + log (2 ^ (s - 1)) - log √π =
    (fun s ↦ log (Γ (s / 2)) + log (Γ (s / 2 + 1 / 2)) + s * log 2 - log (2 * √π)) s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
⊢ ↑n ^ s * ∫ (x : ℝ) in 0..1, ↑x ^ (s - 1) * (1 - ↑x) ^ (↑n + 1 - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)

Tactic:
real_smul,

Goal state after:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
⊢ ↑n ^ s * ∫ (x : ℝ) in 0..1, ↑x ^ (s - 1) * (1 - ↑x) ^ (↑n + 1 - 1) =
    ↑↑n * ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)