mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: case inr.refine_1
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : eval μ (cyclotomic m R) ^ (p ^ k - p ^ (k - 1)) = 0
⊢ IsPrimitiveRoot μ m

Tactic:
replace h := eq_zero_of_pow_eq_zero h

Goal state after:
case inr.refine_1
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : eval μ (cyclotomic m R) = 0
⊢ IsPrimitiveRoot μ m
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
⊢ eval 1 (cyclotomic n ℤ) = 1 ∨ eval 1 (cyclotomic n ℤ) = -1

Tactic:
← Int.natAbs_eq_natAbs_iff,

Goal state after:
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
⊢ (eval 1 (cyclotomic n ℤ)).natAbs = Int.natAbs 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    ↑p ^ padicValNat p n *
      ∏ x ∈ n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
⊢ {n} ⊆ n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n))

Tactic:
simp only [singleton_subset_iff, mem_sdiff, mem_erase, Ne, mem_divisors, dvd_refl,
        true_and, mem_image, mem_range, not_exists, not_and]

Goal state after:
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this✝ : Fact (Nat.Prime p)
this :
  ↑n =
    ↑p ^ padicValNat p n *
      ∏ x ∈ n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
⊢ (¬n = 1 ∧ ¬n = 0) ∧ ∀ x < padicValNat p n, ¬p ^ (x + 1) = n
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: S T : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
this : {b | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1} = {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}
b : B
h : b ∈ adjoin A ({b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})
⊢ b ∈ adjoin ↥(adjoin A {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) {b | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}

Tactic:
adjoin_union_eq_adjoin_adjoin,

Goal state after:
S T : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
this : {b | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1} = {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}
b : B
h :
  b ∈
    Subalgebra.restrictScalars A (adjoin ↥(adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) {b | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})
⊢ b ∈ adjoin ↥(adjoin A {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) {b | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
b : ZMod N
hb_ne : b ≠ 0
hb : e.mulShift b = 1
⊢ ∃ d, d ∣ N ∧ d < N ∧ e.mulShift ↑d = 1

Tactic:
obtain ⟨d, hd, u, hu, rfl⟩ := b.eq_unit_mul_divisor

Goal state after:
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * ↑d ≠ 0
hb : e.mulShift (u * ↑d) = 1
⊢ ∃ d, d ∣ N ∧ d < N ∧ e.mulShift ↑d = 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
⊢ ↑(toCircle j) = cexp (2 * ↑π * I * ↑j.val / ↑N)

Tactic:
← toCircle_natCast,

Goal state after:
N : ℕ
inst✝ : NeZero N
j : ZMod N
⊢ ↑(toCircle j) = ↑(toCircle ↑j.val)
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✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x✝ : ↥(nonZeroDivisors (CyclotomicRing n A K))
x : CyclotomicRing n A K
hx : x ∈ nonZeroDivisors (CyclotomicRing n A K)
⊢ IsUnit ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑⟨x, hx⟩)

Tactic:
by
    rw [isUnit_iff_ne_zero]
    apply map_ne_zero_of_mem_nonZeroDivisors
    · apply adjoin_algebra_injective
    · exact hx

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ (changeLevel ⋯) χ = χ

Tactic:
simp [changeLevel, ZMod.unitsMap]

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

Goal state before:
pp: case pos
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ ^ 2 = 1
x : M
hx : IsUnit x
⊢ 1 x = 1

Tactic:
MulChar.one_apply hx

Goal state after:
case pos
M : Type u_4
R : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
χ : MulChar M R
h : χ ^ 2 = 1
x : M
hx : IsUnit x
⊢ 1 = 1
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: A : Type u
B : Type v
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension {n₁} A ↥C₁
h₂ : IsCyclotomicExtension {n₂} A ↥C₂
inst✝¹ : NeZero n₁
inst✝ : NeZero n₂
ζ₁ : ↥C₁
ζ₂ : ↥C₂
hζ₁ : IsPrimitiveRoot ((algebraMap (↥C₁) B) ζ₁) n₁
hζ₂ : IsPrimitiveRoot ((algebraMap (↥C₂) B) ζ₂) n₂
hζ :
  IsPrimitiveRoot
    ((algebraMap (↥C₁) B) ζ₁ ^ (n₁ / n₁.factorizationLCMLeft n₂) *
      (algebraMap (↥C₂) B) ζ₂ ^ (n₂ / n₁.factorizationLCMRight n₂))
    (n₁.lcm n₂)
⊢ IsCyclotomicExtension {n₁.lcm n₂} A ↥(A[(algebraMap (↥C₂) B) ζ₂] ⊔ A[(algebraMap (↥C₁) B) ζ₁])

Tactic:
← adjoin_union,

Goal state after:
A : Type u
B : Type v
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension {n₁} A ↥C₁
h₂ : IsCyclotomicExtension {n₂} A ↥C₂
inst✝¹ : NeZero n₁
inst✝ : NeZero n₂
ζ₁ : ↥C₁
ζ₂ : ↥C₂
hζ₁ : IsPrimitiveRoot ((algebraMap (↥C₁) B) ζ₁) n₁
hζ₂ : IsPrimitiveRoot ((algebraMap (↥C₂) B) ζ₂) n₂
hζ :
  IsPrimitiveRoot
    ((algebraMap (↥C₁) B) ζ₁ ^ (n₁ / n₁.factorizationLCMLeft n₂) *
      (algebraMap (↥C₂) B) ζ₂ ^ (n₂ / n₁.factorizationLCMRight n₂))
    (n₁.lcm n₂)
⊢ IsCyclotomicExtension {n₁.lcm n₂} A ↥(adjoin A ({(algebraMap (↥C₂) B) ζ₂} ∪ {(algebraMap (↥C₁) B) ζ₁}))
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ s ⩿ insert a s

Tactic:
simp [← coe_wcovBy_coe]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ s.erase a ⩿ s

Tactic:
simp [← coe_wcovBy_coe]

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

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
p : ℝ
hp : 1 < p
x : E
hx : x = 0
⊢ ContinuousAt (fun x ↦ p * ‖x‖ ^ (p - 1)) 0

Tactic:
fun_prop (discharger := simp [hp.le])

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

Goal state before:
pp: case mpr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ t ⊆ s ∧ #(s \ t) = 1 → ∃ a ∉ t, insert a t = s

Tactic:
· simp_rw [card_eq_one]
    rintro ⟨hts, a, ha⟩
    refine ⟨a, (mem_sdiff.1 <| superset_of_eq ha <| mem_singleton_self _).2, ?_⟩
    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
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
k : ZMod N
⊢ 𝓕 (⇑χ) k = χ⁻¹ (-k) * gaussSum χ stdAddChar

Tactic:
by
  rw [fourierTransform_eq_gaussSum_mulShift, gaussSum_mulShift_of_isPrimitive _ hχ]

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
inst✝ : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
a : Fin (Module.finrank 𝕜 E) → E := fun i ↦ ↑√(⋯.eigenvalues ⋯ i) • (⋯.eigenvectorBasis ⋯) i
x✝ : E
⊢ T x✝ = ∑ x, ⟪(⋯.eigenvectorBasis ⋯) x, x✝⟫ • ↑(⋯.eigenvalues ⋯ x) • (⋯.eigenvectorBasis ⋯) x

Tactic:
← hT.isSymmetric.apply_eigenvectorBasis,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
a : Fin (Module.finrank 𝕜 E) → E := fun i ↦ ↑√(⋯.eigenvalues ⋯ i) • (⋯.eigenvectorBasis ⋯) i
x✝ : E
⊢ T x✝ = ∑ x, ⟪(⋯.eigenvectorBasis ⋯) x, x✝⟫ • ↑T ((⋯.eigenvectorBasis ⋯) x)
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
⊢ M.PosSemidef ↔ ∃ m v, M = ∑ i, vecMulVec (v i) (star (v i))

Tactic:
rw [← isPositive_toEuclideanLin_iff, ← isPositive_toContinuousLinearMap_iff,
    isPositive_iff_eq_sum_rankOne]

Goal state after:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : Type u_4
inst✝ : Finite n
M : Matrix n n 𝕜
this : Fintype n
⊢ (∃ m u, toContinuousLinearMap (toEuclideanLin M) = ∑ i, ((rankOne 𝕜) (u i)) (u i)) ↔
    ∃ m v, M = ∑ i, vecMulVec (v i) (star (v i))
Module: Mathlib.Dynamics.BirkhoffSum.Average

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

Tactic:
inv_mul_cancel₀ hn,

Goal state after:
R : Type u_1
α : Type u_2
M : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : α → α
g : α → M
h : g ∘ f = g
n : ℕ
hn : ↑n ≠ 0
x : α
⊢ 1 • g x = g x
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
E' : Submodule 𝕜 E
F' : Submodule 𝕜 F
iE' : Module.Finite 𝕜 ↥E'
iF' : Module.Finite 𝕜 ↥F'
y : ↥E' ⊗[𝕜] ↥F'
hz : {(mapIncl E' F') y} ⊆ ↑(mapIncl E' F').range
e : OrthonormalBasis (Fin (finrank 𝕜 ↥E')) 𝕜 ↥E'
f : OrthonormalBasis (Fin (finrank 𝕜 ↥F')) 𝕜 ↥F'
hx : ∀ i ∈ Finset.univ, ‖((e.toBasis.tensorProduct f.toBasis).repr y) i‖ ^ 2 = 0
i : Fin (finrank 𝕜 ↥E')
j : Fin (finrank 𝕜 ↥F')
⊢ ((e.toBasis.tensorProduct f.toBasis).repr y) (i, j) = 0

Tactic:
simpa using hx (i, j)

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

Goal state before:
pp: 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) = ∞
this : ∀ (a : ℕ), ∑' (k : ℕ), μ (S (2 * k + 1 + a) \ S (2 * k + a)) ≠ ∞
⊢ ∑' (k : ℕ), μ (S (2 * k + 1) \ S (2 * k)) ≠ ∞

Tactic:
by simpa using this 0

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

Tactic:
have h := (IsometryEquiv.vaddConst p)
    |>.measurePreserving_euclideanHausdorffMeasure (finrank ℝ V) |>.map_eq
  rw [InnerProductSpace.euclideanHausdorffMeasure_eq_volume] at h
  exact h.symm

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

Goal state before:
pp: case inl
ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : IsEmpty ι
⊢ ↑(Fintype.card ι) = 0

pp: case inl
ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : IsEmpty ι
⊢ (Metric.ball x r).Subsingleton

Tactic:
Nat.cast_eq_zero,

Goal state after:
case inl
ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : IsEmpty ι
⊢ Fintype.card ι = 0

case inl
ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : IsEmpty ι
⊢ (Metric.ball x r).Subsingleton
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: case pos
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
h : f.ker = ⊥
hrank : finrank ℝ ↥f.range = finrank ℝ U
bv : OrthonormalBasis (Fin (finrank ℝ U)) ℝ ↥f.range
g : U ≃ₗᵢ[ℝ] ↥f.range := (stdOrthonormalBasis ℝ U).equiv bv (Equiv.refl (Fin (finrank ℝ U)))
⊢ ENNReal.ofReal (g.symm.toLinearIsometry.toLinearMap ∘ₗ f.rangeRestrict).normDet * μH[↑(finrank ℝ U)] s =
    ENNReal.ofReal f.normDet * μH[↑(finrank ℝ U)] s

Tactic:
normDet_comp_of_finrank_eq _ _ hrank.symm,

Goal state after:
case pos
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
h : f.ker = ⊥
hrank : finrank ℝ ↥f.range = finrank ℝ U
bv : OrthonormalBasis (Fin (finrank ℝ U)) ℝ ↥f.range
g : U ≃ₗᵢ[ℝ] ↥f.range := (stdOrthonormalBasis ℝ U).equiv bv (Equiv.refl (Fin (finrank ℝ U)))
⊢ ENNReal.ofReal (g.symm.toLinearIsometry.normDet * f.rangeRestrict.normDet) * μH[↑(finrank ℝ U)] s =
    ENNReal.ofReal f.normDet * μH[↑(finrank ℝ U)] s
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
c : ℝ
hc : c < 0
⊢ IsUnit (f - (algebraMap ℝ (H →L[𝕜] H)) c)

Tactic:
sub_eq_add_neg,

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
c : ℝ
hc : c < 0
⊢ IsUnit (f + -(algebraMap ℝ (H →L[𝕜] H)) c)
Module: Mathlib.Analysis.InnerProductSpace.Trace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype ι
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
i : ι
⊢ (b.repr (T (b i))).ofLp i = ⟪b i, T (b i)⟫_𝕜

Tactic:
b.repr_apply_apply

Goal state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype ι
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
i : ι
⊢ ⟪b i, T (b i)⟫_𝕜 = ⟪b i, T (b i)⟫_𝕜
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: 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 : X ≃ᵢ Y
d : ℝ
⊢ Measure.map ⇑e μH[d] = μH[d]

Tactic:
e.isometry.map_hausdorffMeasure (Or.inr e.surjective),

Goal state after:
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 : X ≃ᵢ Y
d : ℝ
⊢ μH[d].restrict (range ⇑e) = μH[d]
Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded

Goal state before:
pp: case h
𝕜 : 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
n : ℕ
a✝ : True
⊢ True ∧ c ^ n • b n ⊆ b n

Tactic:
exact ⟨trivial, (bE1 n).2 _ (by grw [norm_pow, hc1, one_pow])⟩

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

Goal state before:
pp: E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
x : ℝ
⊢ ‖LinearMap.id x‖ * (‖v‖⁻¹ * ‖v‖) = ‖x‖

Tactic:
inv_mul_cancel₀ hn,

Goal state after:
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
x : ℝ
⊢ ‖LinearMap.id x‖ * 1 = ‖x‖
Module: Mathlib.Analysis.LocallyConvex.WeakSpace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : (toWeakSpace 𝕜 E).toEquiv x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
this : ContinuousSMul ℝ E
⊢ ?m.187 ∉ closure s

Tactic:
simpa using hx

Goal state after:
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
H : SeparatingDual 𝕜₂ F
A B : E →SWOT[σ] F
h : ∀ (x : E) (y : F⋆), y (A x) = y (B x)
⊢ ∀ (x : E), A x = B x

Tactic:
← (separatingDual_iff_injective.mp H).eq_iff,

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜₁ E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜₂ F
H : SeparatingDual 𝕜₂ F
A B : E →SWOT[σ] F
h : ∀ (x : E) (y : F⋆), y (A x) = y (B x)
⊢ ∀ (x : E), (ContinuousLinearMap.coeLM 𝕜₂).flip (A x) = (ContinuousLinearMap.coeLM 𝕜₂).flip (B x)
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case neg.mpr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
h : SameRay ℝ x y
⊢ 0 ≤ ⟪x, y⟫ ∧ (o.areaForm x) y = 0

Tactic:
obtain ⟨r, hr, rfl⟩ := h.exists_nonneg_left hx

Goal state after:
case neg.mpr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : ¬x = 0
r : ℝ
hr : 0 ≤ r
h : SameRay ℝ x (r • x)
⊢ 0 ≤ ⟪x, r • x⟫ ∧ (o.areaForm x) (r • x) = 0
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
e_dual : StrongDual 𝕜 F ≃ StrongDual 𝕜 E
he : ∀ (f : StrongDual 𝕜 F), ↑(e_dual f) = e.dualMap ↑f
f : StrongDual 𝕜 E
⊢ ↑(e_dual.symm f) = e.symm.dualMap ↑f

Tactic:
simp only [DFunLike.ext'_iff, ContinuousLinearMap.coe_coe] at he ⊢

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
e_dual : StrongDual 𝕜 F ≃ StrongDual 𝕜 E
f : StrongDual 𝕜 E
he : ∀ (f : StrongDual 𝕜 F), ⇑(e_dual f) = ⇑(e.dualMap ↑f)
⊢ ⇑(e_dual.symm f) = ⇑(e.symm.dualMap ↑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)
a x y : E
⊢ ↑(‖a‖ ^ 2) * (o.kahler x) y = ↑‖a‖ ^ 2 * (o.kahler x) y

Tactic:
· norm_cast

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
this : EqOn (fun t ↦ ↑t ^ (s - 1) • f (a * t)) (fun t ↦ ↑a ^ (1 - s) • (fun u ↦ ↑u ^ (s - 1) • f u) (a * t)) (Ioi 0)
⊢ (↑a ^ (1 - s) * ↑a⁻¹) • ∫ (x : ℝ) in Ioi 0, ↑x ^ (s - 1) • f x = ↑a ^ (-s) • ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f t

Tactic:
sub_eq_add_neg,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this : EqOn (fun t ↦ ↑t ^ (s - 1) • f (a * t)) (fun t ↦ ↑a ^ (1 - s) • (fun u ↦ ↑u ^ (s - 1) • f u) (a * t)) (Ioi 0)
⊢ (↑a ^ (1 + -s) * ↑a⁻¹) • ∫ (x : ℝ) in Ioi 0, ↑x ^ (s - 1) • f x = ↑a ^ (-s) • ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f t
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: z : ℂ
hz : 1 + -z ∈ slitPlane
x✝ : ℝ
⊢ 1 - x✝ • z = 1 + x✝ • -z

Tactic:
sub_eq_add_neg,

Goal state after:
z : ℂ
hz : 1 + -z ∈ slitPlane
x✝ : ℝ
⊢ 1 + -(x✝ • z) = 1 + x✝ • -z
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:
convert! norm_sub_norm_le 1 (-(t * z))

Goal state after:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 = ‖1‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)

Tactic:
let f (z : ℂ) : ℂ := log (1 + z) - logTaylor (n + 1) z

Goal state after:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z ↦ log (1 + z) - logTaylor (n + 1) z
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: n : ℕ
ih : ContinuousAt Gamma (-(↑n + 1))
⊢ ContinuousAt Gamma (-↑n)

Tactic:
suffices ContinuousAt (fun s ↦ Gamma (s - 1 + 1)) (-n) by simpa using this

Goal state after:
n : ℕ
ih : ContinuousAt Gamma (-(↑n + 1))
⊢ ContinuousAt (fun s ↦ Gamma (s - 1 + 1)) (-↑n)