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

Goal state before:
pp: S : Set ℕ
K : Type w
inst✝¹ : Field K
inst✝ : IsSepClosed K
h : ∀ a ∈ S, a ≠ 0 → NeZero ↑a
a : ℕ
ha : a ∈ S
ha' : a ≠ 0
this : NeZero ↑a
⊢ ∃ r, IsPrimitiveRoot r a

Tactic:
obtain ⟨r, hr⟩ := IsSepClosed.exists_aeval_eq_zero K _
    (degree_cyclotomic_pos a K (Nat.pos_of_ne_zero ha')).ne' (separable_cyclotomic a K)

Goal state after:
S : Set ℕ
K : Type w
inst✝¹ : Field K
inst✝ : IsSepClosed K
h : ∀ a ∈ S, a ≠ 0 → NeZero ↑a
a : ℕ
ha : a ∈ S
ha' : a ≠ 0
this : NeZero ↑a
r : K
hr : (aeval r) (cyclotomic a K) = 0
⊢ ∃ r, IsPrimitiveRoot r a
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ χ.conductor = 0 ↔ n = 0

Tactic:
refine ⟨?_, ?_⟩
  · contrapose!
    exact fun h ↦ @conductor_ne_zero _ _ _ χ ⟨h⟩
  · rintro rfl
    exact Nat.sInf_eq_zero.mpr <| Or.inl <| level_mem_conductorSet χ

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

Goal state before:
pp: N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
u : (ZMod N)ˣ
hu : ↑(ZMod.castHom hd (ZMod d)) ↑u = 1
⊢ ↑d ∣ ↑(↑u).val - 1

Tactic:
have : ZMod.castHom hd (ZMod d) u.val = ((u.val.val : ℤ) : ZMod d) := by simp

Goal state after:
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
u : (ZMod N)ˣ
hu : ↑(ZMod.castHom hd (ZMod d)) ↑u = 1
this : (ZMod.castHom hd (ZMod d)) ↑u = ↑↑(↑u).val
⊢ ↑d ∣ ↑(↑u).val - 1
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 χ ψ
⊢ gaussSum χ ψ ^ p ^ (n + 1) = χ (↑p ^ (n + 1)) * gaussSum χ ψ

Tactic:
pow_succ,

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 χ ψ
⊢ gaussSum χ ψ ^ (p ^ n * p) = χ (↑p ^ (n + 1)) * gaussSum χ ψ
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 ^ n) ^ p * χ ↑p * gaussSum χ ψ = χ (↑p ^ (n + 1)) * gaussSum χ ψ

Tactic:
pow_succ,

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 * χ ↑p * gaussSum χ ψ = χ (↑p ^ n * ↑p) * gaussSum χ ψ
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝⁶ : NeZero N
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
R : Type u_2
inst✝³ : Ring R
inst✝² : Module ℂ R
inst✝¹ : Module R E
inst✝ : IsScalarTower ℂ R E
Φ : ZMod N → R
e : E
⊢ (𝓕 fun j ↦ Φ j • e) = fun k ↦ 𝓕 Φ k • e

Tactic:
simp only [dft_def, sum_smul, smul_assoc]

Goal state after:
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: case mpr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
hts : t ⊆ s
a : α
ha : s \ t = {a}
⊢ insert a t = s

Tactic:
rw [insert_eq, ← ha, sdiff_union_of_subset hts]

Goal state after:
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
⊢ Function.Even (𝓕 Φ) ↔ Function.Even Φ

Tactic:
by
  have h {f : ZMod N → ℂ} (hf : f.Even) : (𝓕 f).Even := by
    simp only [Function.Even, ← congr_fun (dft_comp_neg f), funext hf, implies_true]
  refine ⟨fun hΦ x ↦ ?_, h⟩
  simpa only [neg_neg, smul_right_inj (NeZero.ne (N : ℂ)), dft_dft] using h hΦ (-x)

Goal state after:
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
k : ZMod N
⊢ 𝓕 (⇑χ) k = χ⁻¹ (-k) * gaussSum χ stdAddChar

Tactic:
fourierTransform_eq_gaussSum_mulShift,

Goal state after:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
k : ZMod N
⊢ gaussSum χ (stdAddChar.mulShift (-k)) = χ⁻¹ (-k) * gaussSum χ stdAddChar
Module: Mathlib.Analysis.InnerProductSpace.ExteriorPower

Goal state before:
pp: case neg
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
ι : Type u_2
inst✝ : LinearOrder ι
v : ι → E
hv : Orthonormal ℝ v
s t : ↑(Set.powersetCard ι n)
h : ¬s = t
⊢ (of fun i j ↦
        ⟪(v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm s)) j, (v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm t)) i⟫).det =
    0

Tactic:
obtain ⟨x, hxt, hxs⟩ := (Set.powersetCard.exists_mem_notMem_iff_ne t s).mp (.symm h)

Goal state after:
case neg
n : ℕ
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
ι : Type u_2
inst✝ : LinearOrder ι
v : ι → E
hv : Orthonormal ℝ v
s t : ↑(Set.powersetCard ι n)
h : ¬s = t
x : ι
hxt : x ∈ t
hxs : x ∉ s
⊢ (of fun i j ↦
        ⟪(v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm s)) j, (v ∘ ⇑(Set.powersetCard.ofFinEmbEquiv.symm t)) i⟫).det =
    0
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 ι
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp : (↑#ι).HolderConjugate p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
this : Nontrivial ι
h0 : 1 < ↑#ι
h1 : 0 < ↑#ι - 1
h2 : 0 ≤ 1 / (↑#ι - 1)
h3 : (↑#ι - 1) * (1 / (↑#ι - 1)) ≤ 1
⊢ p * (↑#ι - 1) = ↑#ι

Tactic:
rw [mul_comm, hp.sub_one_mul_conj]

Goal state after:
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 a, a⟫

Tactic:
← hT.isIdempotentElem

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 * T) a, a⟫
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 a - p a, a⟫
hh : ∀ {T : E →ₗ[𝕜] E}, T.IsSymmetricProjection → re ⟪T a, a⟫ = ‖T a‖ ^ 2
⊢ a ∈ q.range

Tactic:
inner_sub_left,

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
hh : ∀ {T : E →ₗ[𝕜] E}, T.IsSymmetricProjection → re ⟪T a, a⟫ = ‖T a‖ ^ 2
h2 : 0 ≤ re (⟪q a, a⟫ - ⟪p a, a⟫)
⊢ a ∈ q.range
Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram

Goal state before:
pp: V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(↑(continuousLinearMapOfBilin B)).range
v w : V
mem_w_orthogonal : w ∈ (↑(continuousLinearMapOfBilin B)).rangeᗮ
⊢ ⟪w, v⟫ = 0

Tactic:
rcases coercive with ⟨C, C_pos, coercivity⟩

Goal state after:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(↑(continuousLinearMapOfBilin B)).range
v w : V
mem_w_orthogonal : w ∈ (↑(continuousLinearMapOfBilin B)).rangeᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
⊢ ⟪w, v⟫ = 0
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 x = g (f^[n] x) - g x

Tactic:
by
  rw [← sub_eq_iff_eq_add.2 (birkhoffSum_succ f g n x),
    ← sub_eq_iff_eq_add.2 (birkhoffSum_succ' f g n x),
    ← sub_add, ← sub_add, sub_add_comm]

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

Goal state before:
pp: case neg.inr
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
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hnp : 0 < ↑n - ↑p
hp : 1 < p
q : ℝ := (↑p).conjExponent
⊢ eLpNorm u (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ

Tactic:
have hq : Real.HolderConjugate p q := .conjExponent hp

Goal state after:
case neg.inr
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
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hnp : 0 < ↑n - ↑p
hp : 1 < p
q : ℝ := (↑p).conjExponent
hq : (↑p).HolderConjugate q
⊢ eLpNorm u (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ
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
⊢ ‖lTensor G g‖ ≤ ‖g‖

Tactic:
lTensor,

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) ∘SL rTensor G g ∘SL ↑↑(commIsometry 𝕜 G E)‖ ≤ ‖g‖
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
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : FiniteDimensional 𝕜 G
f : E →ₗ[𝕜] F
⊢ adjoint (rTensor G f) = rTensor G (adjoint f)

Tactic:
by simp [rTensor]

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

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

Tactic:
simp only [le_iInf_iff, iSup_le_iff, ENNReal.coe_le_coe]

Goal state after:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
⊢ ∀ (i : ℝ≥0), μH[↑i] s = 0 → ∀ (i_2 : ℝ≥0), μH[↑i_2] s = ∞ → i_2 ≤ i
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : EMetricSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : EMetricSpace Y
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℕ
hf : Isometry f
⊢ map f μHE[d] = μHE[d].restrict (Set.range f)

Tactic:
by
  simp_rw [euclideanHausdorffMeasure_def]
  rw [Measure.map_smul, map_hausdorffMeasure hf (by simp), Measure.restrict_smul]

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

Goal state before:
pp: X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
h : r < dimH s
⊢ ∃ x ∈ s, ∀ t ∈ 𝓝[s] x, r < dimH t

Tactic:
contrapose! h; choose! t htx htr using h
  rcases countable_cover_nhdsWithin htx with ⟨S, hSs, hSc, hSU⟩
  calc
    dimH s ≤ dimH (⋃ x ∈ S, t x) := dimH_mono hSU
    _ = ⨆ x ∈ S, dimH (t x) := dimH_bUnion hSc _
    _ ≤ r := iSup₂_le fun x hx => htr x <| hSs hx

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

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s t : Set X
r : ℝ≥0∞
r0 : 0 < r
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
ε : ℝ≥0∞
left✝ : 0 < ε
εr : ε < r
⊢ ∀ (u : Set X), (s ∩ u).Nonempty → (t ∩ u).Nonempty → extend (fun s x ↦ m s) u = ∞

Tactic:
rintro u ⟨x, hxs, hxu⟩ ⟨y, hyt, hyu⟩

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
s t : Set X
r : ℝ≥0∞
r0 : 0 < r
hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y
ε : ℝ≥0∞
left✝ : 0 < ε
εr : ε < r
u : Set X
x : X
hxs : x ∈ s
hxu : x ∈ u
y : X
hyt : y ∈ t
hyu : y ∈ u
⊢ extend (fun s x ↦ m s) u = ∞
Module: Mathlib.Analysis.InnerProductSpace.StarOrder

Goal state before:
pp: 𝕜 : Type u_1
H : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : CompleteSpace H
inst✝¹ : Algebra ℝ (H →L[𝕜] H)
inst✝ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
f : H →L[𝕜] H
hf : f.IsPositive
⊢ SpectrumRestricts f ⇑ContinuousMap.realToNNReal

Tactic:
SpectrumRestricts.nnreal_iff

Goal state after:
𝕜 : Type u_1
H : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : CompleteSpace H
inst✝¹ : Algebra ℝ (H →L[𝕜] H)
inst✝ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
f : H →L[𝕜] H
hf : f.IsPositive
⊢ ∀ x ∈ spectrum ℝ f, 0 ≤ 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
⊢ 0 < ‖r‖₊ ^ d

Tactic:
· simp [pos_iff_ne_zero, hr]

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
⊢ μH[↑(finrank ℝ E)] K < ∞

Tactic:
set e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq (by simp)
    suffices μH[finrank ℝ E] (e '' K) < ⊤ by
      rw [← e.symm_image_image K]
      apply lt_of_le_of_lt <| e.symm.lipschitz.hausdorffMeasure_image_le (by simp) (e '' K)
      rw [ENNReal.rpow_natCast]
      exact ENNReal.mul_lt_top (ENNReal.pow_lt_top ENNReal.coe_lt_top) this
    conv_lhs => congr; congr; rw [← Fintype.card_fin (finrank ℝ E)]
    rw [hausdorffMeasure_pi_real]
    exact (hK.image e.continuous).measure_lt_top

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)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ (((map (Fin 2) φ.toLinearEquiv) o).areaForm x) y = ⟪φ (o.rightAngleRotation (φ.symm x)), y⟫

Tactic:
trans ⟪J (φ.symm x), φ.symm y⟫

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ (((map (Fin 2) φ.toLinearEquiv) o).areaForm x) y = ⟪o.rightAngleRotation (φ.symm x), φ.symm y⟫

E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ ⟪o.rightAngleRotation (φ.symm x), φ.symm y⟫ = ⟪φ (o.rightAngleRotation (φ.symm x)), y⟫
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: f : ℕ → ℂ
t : ℂ
hf : (fun n ↦ f n - (1 + t / ↑n)) =o[atTop] fun n ↦ 1 / ↑n
⊢ Tendsto (fun n ↦ f n ^ n) atTop (𝓝 (cexp t))

Tactic:
show (fun n ↦ f n ^ n) = (fun n ↦ (1 + (f n - 1)) ^ n) by ext; simp

Goal state after:
f : ℕ → ℂ
t : ℂ
hf : (fun n ↦ f n - (1 + t / ↑n)) =o[atTop] fun n ↦ 1 / ↑n
⊢ Tendsto (fun n ↦ (1 + (f n - 1)) ^ n) atTop (𝓝 (cexp t))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: u : ℂ
hu : 0 < u.re
⊢ u.betaIntegral 1 = 1 / u

Tactic:
by
  simp_rw [betaIntegral, sub_self, cpow_zero, mul_one]
  rw [integral_cpow (Or.inl _)]
  · rw [ofReal_zero, ofReal_one, one_cpow, zero_cpow, sub_zero, sub_add_cancel]
    rw [sub_add_cancel]
    contrapose! hu; rw [hu, zero_re]
  · rwa [sub_re, one_re, ← sub_pos, sub_neg_eq_add, sub_add_cancel]

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

Goal state before:
pp: case e_a
n : ℕ
L : IntervalIntegrable (fun i ↦ sin i ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun i ↦ sin i ^ n) volume (π / 2) π
⊢ ∫ (x : ℝ) in 0..π / 2, cos x ^ n = ∫ (x : ℝ) in 0..π / 2, sin x ^ n

Tactic:
nth_rw 1 [(by ring : 0 = π / 2 - π / 2)]

Goal state after:
case e_a
n : ℕ
L : IntervalIntegrable (fun i ↦ sin i ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun i ↦ sin i ^ n) volume (π / 2) π
⊢ ∫ (x : ℝ) in π / 2 - π / 2..π / 2, cos x ^ n = ∫ (x : ℝ) in 0..π / 2, sin x ^ n
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
α : Type u_4
l : Filter α
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
⊢ (asymptoticNhds k P v).NeBot

Tactic:
have ⟨p⟩ : Nonempty P := inferInstance
  rw [asymptoticNhds_eq_smul_vadd v p]
  infer_instance

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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
⊢ Tendsto (fun n ↦ ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) atTop (𝓝 s.GammaIntegral)

Tactic:
have f_tends : ∀ x : ℝ, x ∈ Ioi (0 : ℝ) →
      Tendsto (fun n : ℕ => f n x) atTop (𝓝 <| ↑(Real.exp (-x)) * (x : ℂ) ^ (s - 1)) := by
    intro x hx
    apply Tendsto.congr'
    · change ∀ᶠ n : ℕ in atTop, ↑((1 - x / n) ^ n) * (x : ℂ) ^ (s - 1) = f n x
      filter_upwards [eventually_ge_atTop ⌈x⌉₊] with n hn
      rw [Nat.ceil_le] at hn
      dsimp only [f]
      rw [indicator_of_mem]
      exact ⟨hx, hn⟩
    · simp_rw [mul_comm]
      refine (Tendsto.comp (continuous_ofReal.tendsto _) ?_).const_mul _
      convert! Real.tendsto_one_add_div_pow_exp (-x) using 1
      ext1 n
      rw [neg_div, ← sub_eq_add_neg]

Goal state after:
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n ↦ f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
⊢ Tendsto (fun n ↦ ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) atTop (𝓝 s.GammaIntegral)
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : IsTopologicalAddGroup M
inst✝⁵ : ContinuousSMul R M
inst✝⁴ : ContinuousSMul Rᵐᵒᵖ M
inst✝³ : Algebra ℚ R
inst✝² : Module ℚ M
inst✝¹ : T2Space R
inst✝ : T2Space M
x : R
⊢ exp (inl x) = inl (exp x)

Tactic:
rw [exp_def_of_smul_comm, snd_inl, fst_inl, smul_zero, inr_zero, add_zero]

Goal state after:
case hx
R : Type u_3
M : Type u_4
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : IsTopologicalAddGroup M
inst✝⁵ : ContinuousSMul R M
inst✝⁴ : ContinuousSMul Rᵐᵒᵖ M
inst✝³ : Algebra ℚ R
inst✝² : Module ℚ M
inst✝¹ : T2Space R
inst✝ : T2Space M
x : R
⊢ MulOpposite.op (inl x).fst • (inl x).snd = (inl x).fst • (inl x).snd
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: case succ
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormOneClass F
inst✝¹ : NormMulClass F
inst✝ : NormedAlgebra ℂ F
x : F
M : ℝ
hM : 0 ≤ M
h : ∀ (z' : ℂ), M ≤ ‖x - (algebraMap ℂ F) z'‖
c : ℂ
n : ℕ
ih : ∀ {p : ℂ[X]}, p.IsMonicOfDegree n → M ^ n ≤ ‖(aeval (x - (algebraMap ℂ F) c)) p‖
p : ℂ[X]
hp : p.IsMonicOfDegree (n + 1)
f₂ : ℂ[X]
hf₂ : f₂.IsMonicOfDegree n
r : ℂ
hf₁ : (X + C r).IsMonicOfDegree 1
H : p = (X + C r) * f₂
H' : ∀ (y : F), (aeval y) (X + C r) = y + (algebraMap ℂ F) r
⊢ M ^ (n + 1) ≤ ‖(aeval (x - (algebraMap ℂ F) c)) p‖

Tactic:
simpa only [pow_succ, mul_comm, H, aeval_mul, H', sub_add, ← map_sub, norm_mul]
      using mul_le_mul (ih hf₂) (h (c - r)) hM (norm_nonneg _)

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

Goal state before:
pp: m : Type u_1
𝔸 : Type u_5
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
U A : Matrix m m 𝔸
hy : IsUnit U
u : (Matrix m m 𝔸)ˣ
hu : ↑u = U
⊢ exp (↑u * A * (↑u)⁻¹) = ↑u * exp A * (↑u)⁻¹

Tactic:
by simpa only [Matrix.coe_units_inv] using exp_units_conj u A

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

Goal state before:
pp: case e'_6
z : ℂ
this :
  HasSum
    (fun x ↦ ((z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! + (-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) / 2)
    ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
k : ℕ
⊢ (z * I) ^ (2 * k) / ↑(2 * k)! =
    ((z * I) ^ (2 * k) / ↑(2 * k)! + (-z * I) ^ (2 * k) / ↑(2 * k)!) / 2 +
      ((z * I) ^ (2 * k + 1) / ↑(2 * k + 1)! + (-z * I) ^ (2 * k + 1) / ↑(2 * k + 1)!) / 2

Tactic:
pow_succ,

Goal state after:
case e'_6
z : ℂ
this :
  HasSum
    (fun x ↦ ((z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! + (-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) / 2)
    ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
k : ℕ
⊢ (z * I) ^ (2 * k) / ↑(2 * k)! =
    ((z * I) ^ (2 * k) / ↑(2 * k)! + (-z * I) ^ (2 * k) / ↑(2 * k)!) / 2 +
      ((z * I) ^ (2 * k) * (z * I) / ↑(2 * k + 1)! + (-z * I) ^ (2 * k) * (-z * I) / ↑(2 * k + 1)!) / 2