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

Goal state before:
pp: n : ℕ
inst✝⁷ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : NeZero ↑n
⊢ IsCyclotomicExtension {n} K (CyclotomicField n K)

Tactic:
by
  have : NeZero (n : CyclotomicField n K) :=
    NeZero.nat_of_injective (algebraMap K _).injective
  let := Classical.decEq (CyclotomicField n K)
  have := (degree_cyclotomic_pos n K (NeZero.pos n)).ne'
  obtain ⟨ζ, hζ⟩ :=
    Splits.exists_eval_eq_zero (SplittingField.splits (cyclotomic n K)) (by rwa [degree_map])
  rw [eval_map, ← eval_map, ← IsRoot.def, map_cyclotomic, isRoot_cyclotomic_iff] at hζ
  refine ⟨?_, ?_⟩
  · simp only [mem_singleton_iff, forall_eq]
    exact fun _ ↦ ⟨ζ, hζ⟩
  · rw [← Algebra.eq_top_iff, ← SplittingField.adjoin_rootSet, eq_comm]
    exact IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Fintype R
χ : MulChar R ℂ
ψ : AddChar R ℂ
⊢ ∑ x, star (ψ x) * χ⁻¹ x = ∑ x, ψ⁻¹ x * χ⁻¹ x

Tactic:
simp [← starRingEnd_apply, map_neg_eq_conj]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Fintype R
χ : MulChar R ℂ
ψ : AddChar R ℂ
⊢ ∑ x, ψ⁻¹ x * χ⁻¹ x = gaussSum χ⁻¹ ψ⁻¹

Tactic:
by simp [mul_comm, gaussSum]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
n : ℕ
ih : gaussSum χ ψ ^ p ^ n = χ (↑p ^ n) * gaussSum χ ψ
⊢ (χ ^ p) (↑p ^ n) * χ ↑p * gaussSum χ ψ = χ (↑p ^ n) * χ ↑p * gaussSum χ ψ

Tactic:
hχ.pow_char p

Goal state after:
case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
n : ℕ
ih : gaussSum χ ψ ^ p ^ n = χ (↑p ^ n) * gaussSum χ ψ
⊢ χ (↑p ^ n) * χ ↑p * gaussSum χ ψ = χ (↑p ^ n) * χ ↑p * gaussSum χ ψ
Module: Mathlib.Analysis.InnerProductSpace.JointEigenspace

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
A B : E →ₗ[𝕜] E
hA : A.IsSymmetric
hB : B.IsSymmetric
i j : 𝕜 × 𝕜
hij : i ≠ j
v : E
x✝ : v ∈ eigenspace A i.2 ⊓ eigenspace B i.1
hv1 : v ∈ ↑(eigenspace A i.2)
hv2 : v ∈ ↑(eigenspace B i.1)
h₂ : i.2 ≠ j.2
w : E
hw1 : w ∈ ↑(eigenspace A j.2)
hw2 : w ∈ ↑(eigenspace B j.1)
⊢ inner 𝕜 w v = 0

Tactic:
exact hA.orthogonalFamily_eigenspaces.pairwise h₂ hv1 w hw1

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

Goal state before:
pp: case neg
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn : 0 < n
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑n)⁻¹
n' : ℝ≥0 := (↑n).conjExponent
h2p : ↑p < ↑n
⊢ eLpNorm u (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ

Tactic:
have h0n : 2 ≤ n := Nat.succ_le_of_lt <| Nat.one_lt_cast.mp <| hp.trans_lt h2p

Goal state after:
case neg
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn : 0 < n
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑n)⁻¹
n' : ℝ≥0 := (↑n).conjExponent
h2p : ↑p < ↑n
h0n : 2 ≤ n
⊢ eLpNorm u (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ
Module: Mathlib.Analysis.InnerProductSpace.SingularValues

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
this : (adjoint T ∘ₗ T).ker = ⊥ ↔ ¬End.HasEigenvalue (adjoint T ∘ₗ T) 0
⊢ End.HasEigenvalue (adjoint T ∘ₗ T) 0 → ∃ i < finrank 𝕜 E, T.singularValues i ≤ 0

pp: case mpr
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
this : (adjoint T ∘ₗ T).ker = ⊥ ↔ ¬End.HasEigenvalue (adjoint T ∘ₗ T) 0
⊢ (∃ i < finrank 𝕜 E, T.singularValues i ≤ 0) → End.HasEigenvalue (adjoint T ∘ₗ T) 0

Tactic:
· intro h
    obtain ⟨i, hi⟩ := T.isSymmetric_adjoint_comp_self.exists_eigenvalues_eq rfl h
    use i, i.isLt
    simp [RCLike.ofReal_eq_zero.mp hi, T.singularValues_fin rfl]

Goal state after:
case mpr
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
this : (adjoint T ∘ₗ T).ker = ⊥ ↔ ¬End.HasEigenvalue (adjoint T ∘ₗ T) 0
⊢ (∃ i < finrank 𝕜 E, T.singularValues i ≤ 0) → End.HasEigenvalue (adjoint T ∘ₗ T) 0
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
g : E →L[𝕜] F
⊢ ‖↑↑(commIsometry 𝕜 F G) ∘SL rTensor G g ∘SL ↑↑(commIsometry 𝕜 G E)‖ ≤ ‖g‖

Tactic:
← LinearIsometryEquiv.toContinuousLinearMap_toLinearIsometry

Goal state after:
𝕜 : 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
g : E →L[𝕜] F
⊢ ‖(commIsometry 𝕜 F G).toLinearIsometry.toContinuousLinearMap ∘SL
        rTensor G g ∘SL (commIsometry 𝕜 G E).toLinearIsometry.toContinuousLinearMap‖ ≤
    ‖g‖
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: X : Type u_1
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
heq : {0} = parallelepiped ⇑basis
h✝ : volume = volume.addHaarScalarFactor μH[↑0] • μH[↑0]
h : (volume.addHaarScalarFactor μH[↑0] • μH[↑0]) {0} = volume {0}
| volume (parallelepiped ⇑basis)

Tactic:
OrthonormalBasis.volume_parallelepiped

Goal state after:
X : Type u_1
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
heq : {0} = parallelepiped ⇑basis
h✝ : volume = volume.addHaarScalarFactor μH[↑0] • μH[↑0]
h : (volume.addHaarScalarFactor μH[↑0] • μH[↑0]) {0} = volume {0}
| 1
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: 𝕜 : Type u_3
V : Type u_4
P : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedSpace 𝕜 V
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : BorelSpace P
d : ℕ
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
⊢ volume.addHaarScalarFactor μH[↑d] • μH[↑d] (⇑(AffineMap.homothety x c) '' s) =
    ‖c‖₊ ^ d • volume.addHaarScalarFactor μH[↑d] • μH[↑d] s

Tactic:
rw [hausdorffMeasure_homothety_image (by simp) x hc, smul_comm, NNReal.rpow_natCast]

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
h : map ⇑(IsometryEquiv.vaddConst p) μHE[finrank ℝ V] = μHE[finrank ℝ V]
⊢ μHE[finrank ℝ V] = map (⇑(IsometryEquiv.vaddConst p)) volume

Tactic:
InnerProductSpace.euclideanHausdorffMeasure_eq_volume

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
h : map (⇑(IsometryEquiv.vaddConst p)) volume = μHE[finrank ℝ V]
⊢ μHE[finrank ℝ V] = map (⇑(IsometryEquiv.vaddConst p)) volume
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
tfae_1_iff_2 : f.normDet ≠ 0 ↔ f.ker = ⊥
tfae_1_iff_3 : f.normDet ≠ 0 ↔ finrank 𝕜 ↥f.range = finrank 𝕜 U
h : finrank 𝕜 ↥f.range = finrank 𝕜 U
⊢ Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)

Tactic:
← h

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
tfae_1_iff_2 : f.normDet ≠ 0 ↔ f.ker = ⊥
tfae_1_iff_3 : f.normDet ≠ 0 ↔ finrank 𝕜 ↥f.range = finrank 𝕜 U
h : finrank 𝕜 ↥f.range = finrank 𝕜 U
⊢ Nonempty (OrthonormalBasis (Fin (finrank 𝕜 ↥f.range)) 𝕜 ↥f.range)
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
⊢ (-f).normDet = f.normDet

Tactic:
by
  simpa using f.normDet_smul (-1)

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

Goal state before:
pp: case pos
𝕜 : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : InnerProductSpace 𝕜 W
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
hf : f.ker = ⊥
⊢ (g ∘ₗ f).normDet = (g.domRestrict f.range).normDet * f.normDet

Tactic:
let bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
    obtain ⟨bv⟩ := (f.normDet_ne_zero_tfae.out 1 3).mp hf
    by_cases hgf : (g ∘ₗ f).ker = ⊥
    · obtain ⟨bw⟩ := ((g ∘ₗ f).normDet_ne_zero_tfae.out 1 3).mp hgf
      let bw' : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 (g.domRestrict f.range).range :=
        bw.map (LinearIsometryEquiv.ofEq _ _ (by simp [LinearMap.range_comp]))
      rw [(g ∘ₗ f).normDet_eq_norm_det_toMatrix_rangeRestrict bu bw,
        f.normDet_eq_norm_det_toMatrix_rangeRestrict bu bv,
        (g.domRestrict f.range).normDet_eq_norm_det_toMatrix_rangeRestrict bv bw']
      rw [← norm_mul, ← Matrix.det_mul, ← LinearMap.toMatrix_comp]
      rfl
    · have hg : (g.domRestrict f.range).ker ≠ ⊥ := by
        contrapose hf with hgf'
        rw [← LinearMap.ker_rangeRestrict, ← LinearMap.ker_comp_of_ker_eq_bot _ hgf']
        exact hgf
      simp [normDet_eq_zero_iff_ker_ne_bot.mpr hgf, normDet_eq_zero_iff_ker_ne_bot.mpr hg]

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

Goal state before:
pp: case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
t : ℕ → Set X
hst : {x} ⊆ ⋃ n, t n
i✝ : ∀ (n : ℕ), ediam (t n) ≤ 1
m : ℕ
hm : x ∈ t m
⊢ 1 ≤ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), 1

Tactic:
have A : (t m).Nonempty := ⟨x, hm⟩

Goal state after:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
x : X
t : ℕ → Set X
hst : {x} ⊆ ⋃ n, t n
i✝ : ∀ (n : ℕ), ediam (t n) ≤ 1
m : ℕ
hm : x ∈ t m
A : (t m).Nonempty
⊢ 1 ≤ ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), 1
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
f : H
fin : f ∈ (span 𝕜 {x | ∃ x_1 v, (kerFun H x_1) v = x}).topologicalClosureᗮ
x : X
v : V
⊢ (kerFun H x) v ∈ ↑(span 𝕜 {x | ∃ x_1 v, (kerFun H x_1) v = x}).toAddSubmonoid

Tactic:
simp [mem_span_of_mem]

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

Goal state before:
pp: U : Type u_5
V : Type u_6
inst✝⁸ : NormedAddCommGroup U
inst✝⁷ : InnerProductSpace ℝ U
inst✝⁶ : FiniteDimensional ℝ U
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MeasurableSpace U
inst✝² : BorelSpace U
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : U →ₗ[ℝ] V
s : Set U
⊢ ENNReal.ofReal f.normDet * μHE[finrank ℝ U] s = ENNReal.ofReal f.normDet * volume s

Tactic:
InnerProductSpace.euclideanHausdorffMeasure_eq_volume

Goal state after:
U : Type u_5
V : Type u_6
inst✝⁸ : NormedAddCommGroup U
inst✝⁷ : InnerProductSpace ℝ U
inst✝⁶ : FiniteDimensional ℝ U
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MeasurableSpace U
inst✝² : BorelSpace U
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : U →ₗ[ℝ] V
s : Set U
⊢ ENNReal.ofReal f.normDet * volume s = ENNReal.ofReal f.normDet * volume s
Module: Mathlib.Analysis.InnerProductSpace.Trace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
x y : E
⊢ (trace 𝕜 𝕜) ↑(ContinuousLinearMap.toSpanSingleton 𝕜 (((innerSL 𝕜) y) x)) = ⟪y, x⟫_𝕜

Tactic:
simp [trace_eq_sum_inner _ (OrthonormalBasis.singleton Unit 𝕜)]

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

Goal state before:
pp: ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹⁰ : EMetricSpace X
inst✝⁹ : EMetricSpace Y
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : BorelSpace Y
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
K : Set E
hK : IsCompact K
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
this : μH[↑(finrank ℝ E)] (⇑e '' K) < ∞
⊢ μH[↑(finrank ℝ E)] (⇑e.symm '' ⇑e '' K) < ∞

Tactic:
apply lt_of_le_of_lt <| e.symm.lipschitz.hausdorffMeasure_image_le (by simp) (e '' K)

Goal state after:
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹⁰ : EMetricSpace X
inst✝⁹ : EMetricSpace Y
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : MeasurableSpace Y
inst✝⁵ : BorelSpace Y
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
K : Set E
hK : IsCompact K
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ⋯
this : μH[↑(finrank ℝ E)] (⇑e '' K) < ∞
⊢ ↑‖↑e.symm‖₊ ^ ↑(finrank ℝ E) * μH[↑(finrank ℝ E)] (⇑e '' K) < ∞
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
h : ∀ (i : ℕ), ∃ x ∈ c ^ i • b i, f x ∉ V
⊢ False

Tactic:
choose! u hu hu' using h

Goal state after:
𝕜 : 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
⊢ False
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:
Measure.map_apply (AffineMap.homothety_continuous x c).measurable hs,

Goal state after:
𝕜 : 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
⊢ μH[d] (⇑(AffineMap.homothety x c) ⁻¹' s) = (‖c‖₊⁻¹ ^ d • μH[d]) s
Module: Mathlib.Analysis.LocallyConvex.StrongTopology

Goal state before:
pp: R : Type u_1
𝕜₁ : Type u_2
𝕜₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : TopologicalSpace E
inst✝¹² : AddCommGroup F
inst✝¹¹ : TopologicalSpace F
inst✝¹⁰ : IsTopologicalAddGroup F
inst✝⁹ : Semiring R
inst✝⁸ : PartialOrder R
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
inst✝³ : Module R F
inst✝² : ContinuousConstSMul R F
inst✝¹ : LocallyConvexSpace R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) 𝔖
⊢ ∀ (i : Set E × Set F), i.1 ∈ 𝔖 ∧ i.2 ∈ 𝓝 0 ∧ Convex R i.2 → Convex R {f | ∀ x ∈ i.1, f x ∈ id i.2}

Tactic:
rintro ⟨S, V⟩ ⟨_, _, hVconvex⟩ f hf g hg a b ha hb hab x hx

Goal state after:
R : Type u_1
𝕜₁ : Type u_2
𝕜₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : TopologicalSpace E
inst✝¹² : AddCommGroup F
inst✝¹¹ : TopologicalSpace F
inst✝¹⁰ : IsTopologicalAddGroup F
inst✝⁹ : Semiring R
inst✝⁸ : PartialOrder R
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
inst✝³ : Module R F
inst✝² : ContinuousConstSMul R F
inst✝¹ : LocallyConvexSpace R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) 𝔖
S : Set E
V : Set F
left✝¹ : (S, V).1 ∈ 𝔖
left✝ : (S, V).2 ∈ 𝓝 0
hVconvex : Convex R (S, V).2
f : E →SLᵤ[σ, 𝔖] F
hf : f ∈ {f | ∀ x ∈ (S, V).1, f x ∈ id (S, V).2}
g : E →SLᵤ[σ, 𝔖] F
hg : g ∈ {f | ∀ x ∈ (S, V).1, f x ∈ id (S, V).2}
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x : E
hx : x ∈ (S, V).1
⊢ (a • f + b • g) x ∈ id (S, V).2
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case refine_1.inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
h : 0 = ‖o.rightAngleRotationAux₁ x‖
⊢ ‖o.rightAngleRotationAux₁ x‖ ≤ ‖x‖

Tactic:
← h

Goal state after:
case refine_1.inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
h : 0 = ‖o.rightAngleRotationAux₁ x‖
⊢ 0 ≤ ‖x‖
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
⊢ Complex.normSq ((o.kahler x) y) = (‖x‖ * ‖y‖) ^ 2

pp: case ha
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ 0 ≤ ‖(o.kahler x) y‖

pp: case hb
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ 0 ≤ ‖x‖ * ‖y‖

Tactic:
· linear_combination o.normSq_kahler x y

Goal state after:
case ha
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ 0 ≤ ‖(o.kahler x) y‖

case hb
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ 0 ≤ ‖x‖ * ‖y‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: case zero
z : ℂ
⊢ HasDerivAt (logTaylor (0 + 1)) (∑ j ∈ Finset.range 0, (-1) ^ j * z ^ j) z

Tactic:
simp [logTaylor_succ, logTaylor_zero, Pi.add_def, hasDerivAt_const]

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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
⊢ HasDerivAt GammaIntegral (∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) * (↑(Real.log t) * ↑(rexp (-t)))) s

Tactic:
rw [GammaIntegral_eq_mellin]

Goal state after:
s : ℂ
hs : 0 < s.re
⊢ HasDerivAt (mellin fun x ↦ ↑(rexp (-x))) (∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) * (↑(Real.log t) * ↑(rexp (-t)))) s
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
H : -z = 1
⊢ False

Tactic:
rw [neg_eq_iff_eq_neg] at H

Goal state after:
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
H : z = -1
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: case pos
m : ℕ
hs : -↑m ≠ 0
⊢ deriv Gamma (-↑m + 1) = Gamma (-↑m) + -↑m * deriv Gamma (-↑m)

Tactic:
← sub_neg_eq_add,

Goal state after:
case pos
m : ℕ
hs : -↑m ≠ 0
⊢ deriv Gamma (-↑m - -1) = Gamma (-↑m) + -↑m * deriv Gamma (-↑m)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: case neg
s : ℂ
hs : s ≠ 0
h : ∀ (m : ℕ), s ≠ -↑m
⊢ HasDerivWithinAt (fun x ↦ x * Gamma x) (Gamma s + s * deriv Gamma s) {0}ᶜ s

Tactic:
simpa using! HasDerivWithinAt.mul (hasDerivWithinAt_id s {0}ᶜ)
      (differentiableAt_Gamma s h).hasDerivAt.hasDerivWithinAt

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:
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

Goal state after:
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
⊢ ∫ (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)
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
z : ℂ
hz : ‖z‖ < 1
⊢ ‖-log (1 + -z) + logTaylor (n + 1) (-z)‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)

Tactic:
← sub_neg_eq_add,

Goal state after:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
⊢ ‖-log (1 + -z) - -logTaylor (n + 1) (-z)‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)