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

Goal state before:
pp: S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
C : Subalgebra A B
hS : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
⊢ IsCyclotomicExtension S A ↥C ↔ C = adjoin A {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h ▸ isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot S A B hS⟩
  have := congr_arg (Subalgebra.map C.val) ((IsCyclotomicExtension.iff_adjoin_eq_top _ _ _).mp h).2
  rw [← Subalgebra.range_val C, ← Algebra.map_top, ← this, AlgHom.map_adjoin]
  congr; ext
  simp only [Subalgebra.coe_val, ne_eq, ← Subalgebra.coe_eq_one, SubmonoidClass.coe_pow,
    Set.mem_image, Set.mem_ofPred_eq, Subtype.exists, exists_and_left, exists_prop,
    exists_eq_right_right, and_iff_left_iff_imp, forall_exists_index, and_imp]
  exact fun n hn₁ hn₂ hx ↦ h.mem_of_pow_eq_one S C hn₁ hn₂ hx

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
this : NeZero d
hd : d ∣ n
χ₀ : DirichletCharacter R d
hχ₀ : χ = (changeLevel hd) χ₀
⊢ d.gcd χ.conductor ∈ χ.conductorSet

Tactic:
suffices (changeLevel (d.dvd_mul_right χ.conductor)) χ₀ =
      (changeLevel (χ.conductor.dvd_mul_left d)) χ.primitiveCharacter by
    obtain ⟨_, χ₁, hχ₁⟩ := factorsThrough_gcd χ₀ χ.primitiveCharacter this
    refine ⟨Nat.dvd_trans (d.gcd_dvd_left χ.conductor) hd, χ₁, ?_⟩
    rw [changeLevel_trans _ (d.gcd_dvd_left χ.conductor), ← hχ₁, hχ₀]

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
this : NeZero d
hd : d ∣ n
χ₀ : DirichletCharacter R d
hχ₀ : χ = (changeLevel hd) χ₀
⊢ (changeLevel ⋯) χ₀ = (changeLevel ⋯) χ.primitiveCharacter
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
a : Rˣ
⊢ gaussSum χ (ψ.mulShift ↑a) = χ⁻¹ ↑a * (χ ↑a * gaussSum χ (ψ.mulShift ↑a))

Tactic:
inv_apply_eq_inv,

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
a : Rˣ
⊢ gaussSum χ (ψ.mulShift ↑a) = Ring.inverse (χ ↑a) * (χ ↑a * gaussSum χ (ψ.mulShift ↑a))
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
a : Rˣ
⊢ gaussSum χ (ψ.mulShift ↑a) = χ⁻¹ ↑a * gaussSum χ ψ

Tactic:
by
  rw [← gaussSum_mulShift χ ψ a, inv_apply_eq_inv,
    Ring.inverse_mul_cancel_left _ _ (a.isUnit.map χ)]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝² : Field R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
⊢ χ (-1) * gaussSum χ (ψ.mulShift (-1)) = gaussSum χ ψ

Tactic:
← Units.coe_neg_one

Goal state after:
R : Type u
inst✝² : Field R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
⊢ χ ↑(-1) * gaussSum χ (ψ.mulShift ↑(-1)) = gaussSum χ ψ
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : χ (-1) * ↑(Fintype.card R) = 0
hf : gaussSum χ ψ = 0
⊢ False

Tactic:
mul_eq_zero

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : χ (-1) = 0 ∨ ↑(Fintype.card R) = 0
hf : gaussSum χ ψ = 0
⊢ False
Module: Mathlib.Analysis.InnerProductSpace.Affine

Goal state before:
pp: V : Type u_2
P : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
t₁ t₂ : ℝ
h_inner : ⟪b -ᵥ a, c -ᵥ a⟫ = 0
hvec : (AffineMap.lineMap a b) t₁ -ᵥ (AffineMap.lineMap a c) t₂ = t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a)
⊢ (|t₁| * ‖b -ᵥ a‖) ^ 2 - 2 * ((starRingEnd ℝ) t₁ * ⟪b -ᵥ a, t₂ • (c -ᵥ a)⟫) + (|t₂| * ‖c -ᵥ a‖) ^ 2 =
    t₁ ^ 2 * dist a b ^ 2 + t₂ ^ 2 * dist a c ^ 2

Tactic:
inner_smul_right,

Goal state after:
V : Type u_2
P : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
t₁ t₂ : ℝ
h_inner : ⟪b -ᵥ a, c -ᵥ a⟫ = 0
hvec : (AffineMap.lineMap a b) t₁ -ᵥ (AffineMap.lineMap a c) t₂ = t₁ • (b -ᵥ a) - t₂ • (c -ᵥ a)
⊢ (|t₁| * ‖b -ᵥ a‖) ^ 2 - 2 * ((starRingEnd ℝ) t₁ * (t₂ * ⟪b -ᵥ a, c -ᵥ a⟫)) + (|t₂| * ‖c -ᵥ a‖) ^ 2 =
    t₁ ^ 2 * dist a b ^ 2 + t₂ ^ 2 * dist a c ^ 2
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case h₂.hq
ι : 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
x : (i : ι) → A i
X : A i → (a : ι) → A a := ⋯
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ⋯
hk' : 0 ≤ 1 - k * p
⊢ 0 ≤ 1 - k * p

Tactic:
exact hk'

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

Goal state before:
pp: case hz
ι : 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
x : (i : ι) → A i
X : A i → (a : ι) → A a := update x i
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ↑(#s)
hk' : 0 ≤ 1 - k * p
⊢ 0 ≤ 1 - k * p

Tactic:
exact hk'

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
x y z : E
⊢ x * y * z = x * (y * z)

Tactic:
simp_rw [AlgebraOfCoalgebra.mul_def, ← rTensor_tmul, ← comp_apply, ← adjoint_rTensor,
      ← adjoint_comp, ← coassoc_symm, adjoint_comp, adjoint_lTensor, comp_apply,
      ← toLinearEquiv_assocIsometry, ← toLinearEquiv_symm, adjoint_toLinearMap_eq_symm]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
x y z : E
⊢ (adjoint comul)
      ((LinearMap.lTensor E (adjoint comul)) (↑(assocIsometry 𝕜 E E E).symm.symm.toLinearEquiv (x ⊗ₜ[𝕜] y ⊗ₜ[𝕜] z))) =
    (adjoint comul) (x ⊗ₜ[𝕜] (adjoint comul) (y ⊗ₜ[𝕜] z))
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:
← card_add_card_compl s

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 ≤ ↑(#s + #sᶜ)
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : p.IsSymmetricProjection
hq : q.IsSymmetricProjection
x✝ : p ≤ q
a : E
ha : a ∈ p.range
h1 : (q - p).IsSymmetric
h2 : 0 ≤ re ⟪(q - p) a, a⟫
T : E →ₗ[𝕜] E
hT : T.IsSymmetricProjection
⊢ re ⟪T (T a), a⟫ = ‖T a‖ ^ 2

Tactic:
hT.isSymmetric

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
p q : E →ₗ[𝕜] E
hp : p.IsSymmetricProjection
hq : q.IsSymmetricProjection
x✝ : p ≤ q
a : E
ha : a ∈ p.range
h1 : (q - p).IsSymmetric
h2 : 0 ≤ re ⟪(q - p) a, a⟫
T : E →ₗ[𝕜] E
hT : T.IsSymmetricProjection
⊢ re ⟪T a, T a⟫ = ‖T a‖ ^ 2
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
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
S : E →ₗ[𝕜] F
⊢ (LinearMap.adjoint S ∘ₗ S).IsPositive

Tactic:
by
  simpa using! LinearMap.isPositive_one.adjoint_conj S

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : Type u_4
inst✝ : Finite n
M : Matrix n n 𝕜
this : Fintype n
⊢ (toEuclideanLin M).IsPositive ↔ ∃ m v, M = ∑ i, vecMulVec (v i) (star (v i))

Tactic:
← isPositive_toContinuousLinearMap_iff,

Goal state after:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : Type u_4
inst✝ : Finite n
M : Matrix n n 𝕜
this : Fintype n
⊢ (toContinuousLinearMap (toEuclideanLin M)).IsPositive ↔ ∃ m v, M = ∑ i, vecMulVec (v i) (star (v i))
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
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp✝ : (↑(finrank ℝ E)).HolderConjugate p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : (↑#ι).HolderConjugate p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)
hc : 0 < c
h2c : μ = c • Measure.map (⇑e.symm) volume
h3c : ↑c ≠ 0
h0C : C = c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹
hC : C * c ^ p = c * ‖↑e.symm‖₊ ^ p
v : (ι → ℝ) → F := u ∘ ⇑e.symm
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
⊢ (∫⁻ (y : ι → ℝ), ‖fderiv ℝ u (e.symm y)‖ₑ * ‖↑e.symm‖ₑ) ^ p =
    (‖↑e.symm‖ₑ * ∫⁻ (y : ι → ℝ), ‖fderiv ℝ u (e.symm y)‖ₑ) ^ p

Tactic:
rw [lintegral_mul_const, mul_comm]
        fun_prop

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

Goal state before:
pp: 𝕜 : 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
⊢ T.singularValues (finrank 𝕜 ↥T.range) = 0

Tactic:
rw [← Finsupp.notMem_support_iff, support_singularValues]

Goal state after:
𝕜 : 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
⊢ finrank 𝕜 ↥T.range ∉ Finset.range (finrank 𝕜 ↥T.range)
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
x : E ⊗[𝕜] G
⊢ (lTensor E g) x = (LinearMap.lTensor E ↑g) x

Tactic:
simp [lTensor, ← LinearMap.comm_comp_rTensor_comp_comm_eq]

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
A : Type u_6
B : Type u_7
inst✝³ : NormedAddCommGroup A
inst✝² : InnerProductSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : InnerProductSpace 𝕜 B
f₁ : E →L[𝕜] F
f₂ : A →L[𝕜] E
g₁ : G →L[𝕜] H
g₂ : B →L[𝕜] G
⊢ mapL (f₁ ∘SL f₂) (g₁ ∘SL g₂) = mapL f₁ g₁ ∘SL mapL f₂ g₂

Tactic:
by ext; simp [map_map]

Goal state after:
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} = 1
⊢ μHE[0] = μH[0]

Tactic:
CharP.cast_eq_zero,

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} = 1
⊢ μHE[0] = μH[0]
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) = ∞
r : ℕ
⊢ ∑' (k : ℕ), μ (S (2 * k + 1 + r) \ S (2 * k + r)) ≤ μ (⋃ n, S n)

Tactic:
ENNReal.tsum_eq_iSup_nat,

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) = ∞
r : ℕ
⊢ ⨆ i, ∑ a ∈ Finset.range i, μ (S (2 * a + 1 + r) \ S (2 * a + r)) ≤ μ (⋃ n, S n)
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
⊢ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets = dimH s

Tactic:
by
  refine le_antisymm (iSup₂_le fun x _ => ?_) ?_
  · refine limsup_le_of_le isCobounded_le_of_bot ?_
    exact eventually_smallSets.2 ⟨s, self_mem_nhdsWithin, fun t => dimH_mono⟩
  · refine le_of_forall_lt_imp_le_of_dense fun r hr => ?_
    rcases exists_mem_nhdsWithin_lt_dimH_of_lt_dimH hr with ⟨x, hxs, hxr⟩
    refine le_iSup₂_of_le x hxs ?_; rw [limsup_eq]; refine le_sInf fun b hb => ?_
    rcases eventually_smallSets.1 hb with ⟨t, htx, ht⟩
    exact (hxr t htx).le.trans (ht t Subset.rfl)

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
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 = ⊥
⊢ (c • f).normDet = ‖c‖ ^ finrank 𝕜 U * f.normDet

Tactic:
obtain ⟨bv⟩ := (f.normDet_ne_zero_tfae.out 1 3).mp h
    let bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
    let bv' : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 (c • f).range := bv.map
      (LinearIsometryEquiv.ofEq _ _ (LinearMap.range_smul _ _ hc).symm)
    rw [f.normDet_eq_norm_det_toMatrix_rangeRestrict bu bv,
      (c • f).normDet_eq_norm_det_toMatrix_rangeRestrict bu bv', ← norm_pow, ← norm_mul]
    have : finrank 𝕜 U = Fintype.card (Fin (finrank 𝕜 U)) := by simp
    conv in c ^ finrank 𝕜 U => rw [this]
    rw [← Matrix.det_smul, ← map_smul]
    rfl

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
⊢ ⊤ = ⊤.toOuterMeasure

Tactic:
toOuterMeasure_top

Goal state after:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
⊢ ⊤ = ⊤
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
⊢ ↑((↑f).normDet ^ 2) = (ContinuousLinearMap.adjoint f ∘SL f).det

Tactic:
have : CompleteSpace U := FiniteDimensional.complete 𝕜 U
  have : CompleteSpace f.range := FiniteDimensional.complete 𝕜 f.range
  let bu := stdOrthonormalBasis 𝕜 U
  by_cases h : f.ker = ⊥
  · obtain ⟨b⟩ := (f.normDet_ne_zero_tfae.out 1 3).mp h
    have hf : f = f.range.subtypeₗᵢ.toContinuousLinearMap ∘L f.rangeRestrict := rfl
    conv_rhs => rw [hf]
    rw [ContinuousLinearMap.adjoint_comp, ← ContinuousLinearMap.comp_assoc,
      ContinuousLinearMap.comp_assoc (ContinuousLinearMap.adjoint _),
      f.range.subtypeₗᵢ.adjoint_comp_self, ContinuousLinearMap.one_def, ContinuousLinearMap.comp_id,
      ContinuousLinearMap.det, ContinuousLinearMap.toLinearMap_comp, ← det_toMatrix bu.toBasis,
      toMatrix_comp bu.toBasis b.toBasis bu.toBasis, ← ContinuousLinearMap.adjoint_toLinearMap,
      toMatrix_adjoint, f.toLinearMap.normDet_eq_norm_det_toMatrix_rangeRestrict bu b]
    simp [RCLike.conj_mul]
  · trans 0
    · simp [show f.normDet = 0 from (f.normDet_eq_zero_tfae.out 1 0).mp h]
    symm
    rw [det_eq_zero_iff_ker_ne_bot, ContinuousLinearMap.ker_adjoint_comp_self]
    exact h

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
d₁ d₂ : ℝ
h : d₁ ≤ d₂
s : Set X
⊢ μH[d₂] s ≤ μH[d₁] s

Tactic:
rcases h.eq_or_lt with (rfl | h); · exact le_rfl
  rcases hausdorffMeasure_zero_or_top h s with hs | hs <;> simp [hs]

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

Goal state before:
pp: case h
α : Type u_1
R : Type u_2
𝕜₁ : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
inst✝¹² : NormedField 𝕜₁
inst✝¹¹ : NormedField 𝕜₂
inst✝¹⁰ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₃ →+* 𝕜₂
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜₁ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜₂ F
inst✝⁴ : AddCommGroup D
inst✝³ : TopologicalSpace D
inst✝² : Module 𝕜₃ D
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜₂ G
A : (E →SL[σ] F) →ₗ[𝕜₂] D →SL[τ] G
hbound : ∀ (f : D), ∃ s C, ∀ (B : E →SL[σ] F), ∃ g, ∃ (_ : g ∈ s), ‖(A B) f‖ ≤ C • ‖B g‖
f : D
s : Finset E
C : ℝ≥0
h : ∀ (B : E →SL[σ] F), ∃ g, ∃ (_ : g ∈ s), ‖(A B) f‖ ≤ C • ‖B g‖
⊢ (PointwiseConvergenceCLM.seminormFamily τ D G f).comp A ≤ C • s.sup (PointwiseConvergenceCLM.seminormFamily σ E F)

Tactic:
← Seminorm.finset_sup_smul

Goal state after:
case h
α : Type u_1
R : Type u_2
𝕜₁ : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
inst✝¹² : NormedField 𝕜₁
inst✝¹¹ : NormedField 𝕜₂
inst✝¹⁰ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₃ →+* 𝕜₂
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜₁ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜₂ F
inst✝⁴ : AddCommGroup D
inst✝³ : TopologicalSpace D
inst✝² : Module 𝕜₃ D
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜₂ G
A : (E →SL[σ] F) →ₗ[𝕜₂] D →SL[τ] G
hbound : ∀ (f : D), ∃ s C, ∀ (B : E →SL[σ] F), ∃ g, ∃ (_ : g ∈ s), ‖(A B) f‖ ≤ C • ‖B g‖
f : D
s : Finset E
C : ℝ≥0
h : ∀ (B : E →SL[σ] F), ∃ g, ∃ (_ : g ∈ s), ‖(A B) f‖ ≤ C • ‖B g‖
⊢ (PointwiseConvergenceCLM.seminormFamily τ D G f).comp A ≤ s.sup (C • PointwiseConvergenceCLM.seminormFamily σ E F)
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, (LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯) y⟫ =
    -(o.areaForm x) y

Tactic:
exact o.inner_rightAngleRotationAux₁_right x y

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
⊢ 0 ≤ ⟪x, y⟫ ∧ (o.areaForm x) y = 0 ↔ SameRay ℝ x y

Tactic:
by
  by_cases hx : x = 0
  · simp [hx]
  constructor
  · let a : ℝ := (o.basisRightAngleRotation x hx).repr y 0
    let b : ℝ := (o.basisRightAngleRotation x hx).repr y 1
    suffices ↑0 ≤ a * ‖x‖ ^ 2 ∧ b * ‖x‖ ^ 2 = 0 → SameRay ℝ x (a • x + b • J x) by
      rw [← (o.basisRightAngleRotation x hx).sum_repr y]
      simp only [Fin.sum_univ_succ, coe_basisRightAngleRotation, Matrix.cons_val_zero,
        Fin.succ_zero_eq_one', Finset.univ_eq_empty, Finset.sum_empty, areaForm_apply_self,
        map_smul, map_add, real_inner_smul_right, inner_add_right, Matrix.cons_val_one,
        smul_eq_mul, areaForm_rightAngleRotation_right,
        mul_zero, add_zero, zero_add, neg_zero, inner_rightAngleRotation_right,
        real_inner_self_eq_norm_sq]
      exact this
    simp_all
  · intro h
    obtain ⟨r, hr, rfl⟩ := h.exists_nonneg_left hx
    simp only [inner_smul_right, real_inner_self_eq_norm_sq, map_smulₛₗ, areaForm_apply_self,
      smul_eq_mul, mul_zero, and_true]
    positivity

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

Goal state before:
pp: case convert_4
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun x ↦ ↑(rexp (-x))) (𝓝[>] 0) (𝓝 ↑(rexp (-0)))

Tactic:
exact (continuous_ofReal.comp (Real.continuous_exp.comp continuous_neg)).continuousWithinAt

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

Goal state before:
pp: t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 - ‖↑t * z‖ ≤ ‖1 + ↑t * z‖

Tactic:
rw [← norm_neg (t * z), ← sub_neg_eq_add]

Goal state after:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 - ‖-(↑t * z)‖ ≤ ‖1 - -(↑t * z)‖