mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x ↦ |x| ^ (-b)
R S : ℝ
h1 : ⇑(f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ }) =O[atTop] fun x ↦ |x| ^ (-b)
h2 :
  ((fun x ↦ ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    fun x ↦ |x| ^ (-b)
this : (fun x ↦ |x| ^ (-b)) ∘ Neg.neg = fun x ↦ |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x✝ + -S ≤ -x

Tactic:
by linarith [hx.2]

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hi : IsPrimitiveRoot (ζ ^ i) k
a : ℕ
ha : i = i.gcd k * a
b : ℕ
hb : k = i.gcd k * b
this : b = k
⊢ i.Coprime k

Tactic:
rwa [this, eq_comm, Nat.mul_eq_right h0.ne', ← Nat.coprime_iff_gcd_eq_one] at hb

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ p)

Tactic:
have hpos := Nat.pos_of_ne_zero hn

Goal state after:
case neg
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
⊢ minpoly ℤ μ = minpoly ℤ (μ ^ p)
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ : Rˣ
h✝ : IsPrimitiveRoot ζ k
inst✝ : IsDomain R
a b n : ℕ
h : a * b ≡ 1 [MOD n]
x : ↥(primitiveRoots n R)
⊢ (fun x ↦ ⟨↑x ^ a, ⋯⟩) ((fun x ↦ ⟨↑x ^ b, ⋯⟩) x) = x

Tactic:
by ext; simp [← pow_mul, mul_comm b,
    pow_eq_pow_of_modEq h (isPrimitiveRoot_of_mem_primitiveRoots x.2).pow_eq_one]

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: case neg
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
this : NeZero n
⊢ primitiveRoots n K ⊆ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset

Tactic:
have hpos := Nat.pos_of_ne_zero hn

Goal state after:
case neg
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
inst✝ : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
⊢ primitiveRoots n K ⊆ (map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: E : Type u_1
V : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
f : V → E
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
⊢ Tendsto (fun w ↦ ∫ (v : V), 𝐞 (-w v) • f v ∂μ) (cocompact (StrongDual ℝ V)) (𝓝 0)

Tactic:
rw [μ.isAddLeftInvariant_eq_smul volume]
  simp_rw [integral_smul_nnreal_measure]
  rw [← (smul_zero _ : Measure.addHaarScalarFactor μ volume • (0 : E) = 0)]
  apply Tendsto.const_smul
  let A := (InnerProductSpace.toDual ℝ V).symm
  have : (fun w : StrongDual ℝ V ↦ ∫ v, 𝐞 (-w v) • f v) =
      (fun w : V ↦ ∫ v, 𝐞 (-⟪v, w⟫) • f v) ∘ A := by
    ext1 w
    congr 1 with v : 1
    rw [← inner_conj_symm, RCLike.conj_to_real, InnerProductSpace.toDual_symm_apply]
  rw [this]
  exact (tendsto_integral_exp_inner_smul_cocompact f).comp
      A.toHomeomorph.toCocompactMap.cocompact_tendsto'

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: G : Type u_7
G' : Type u_8
inst✝³ : Group G
inst✝² : IsCyclic G
inst✝¹ : Finite G
inst✝ : CommGroup G'
a : G
ha : a ≠ 1
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ orderOf ζ ∣ orderOf g

Tactic:
← hζ.eq_orderOf,

Goal state after:
G : Type u_7
G' : Type u_8
inst✝³ : Group G
inst✝² : IsCyclic G
inst✝¹ : Finite G
inst✝ : CommGroup G'
a : G
ha : a ≠ 1
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ Nat.card G ∣ orderOf g
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ⋯
hP : ∀ (i : Fin p), α i = P.coeff ↑i
hP' : P.degree ≤ ↑(p - 1)
⊢ ∑ i, ↑(α i) * ζ ^ ↑i = 0 ↔ (aeval ζ) P = 0

pp: K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ⋯
hP : ∀ (i : Fin p), α i = P.coeff ↑i
hP' : P.degree ≤ ↑(p - 1)
⊢ (aeval ζ) P = 0 ↔ ∀ (i j : Fin p), α i = α j

Tactic:
· simp [P]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ⋯
hP : ∀ (i : Fin p), α i = P.coeff ↑i
hP' : P.degree ≤ ↑(p - 1)
⊢ (aeval ζ) P = 0 ↔ ∀ (i j : Fin p), α i = α j
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := ⋯
⊢ (algebraMap R K) (x ^ n - y ^ n) = (algebraMap R K) (∏ ζ ∈ nthRootsFinset n 1, (x - ζ * y))

Tactic:
rw [map_sub, map_pow, map_pow, map_prod]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
⊢ (algebraMap R K) x ^ n - (algebraMap R K) y ^ n = ∏ x_1 ∈ nthRootsFinset n 1, (algebraMap R K) (x - x_1 * y)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case h.inr.inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : ∑ i ∈ range n, x ^ i < 0
⊢ 0 < eval x (cyclotomic n R)

Tactic:
· apply pos_of_mul_neg_left
    · rwa [this]
    rw [geom_sum_neg_iff hn'.ne'] at h
    have h2 : 2 ∈ n.properDivisors.erase 1 := by
      rw [Finset.mem_erase, mem_properDivisors]
      exact ⟨by decide, even_iff_two_dvd.mp h.1, hn⟩
    rw [eval_prod, ← Finset.prod_erase_mul _ _ h2]
    apply mul_nonpos_of_nonneg_of_nonpos
    · refine Finset.prod_nonneg fun i hi => le_of_lt ?_
      simp only [Finset.mem_erase, mem_properDivisors] at hi
      refine ih _ hi.2.2.2 (Nat.two_lt_of_ne ?_ hi.2.1 hi.1)
      rintro rfl
      rw [zero_dvd_iff] at hi
      exact hn'.ne' hi.2.2.1
    · simpa only [eval_X, eval_one, cyclotomic_two, eval_add] using h.right.le

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
⊢ ∃ r, x = (-ζ) ^ r

Tactic:
have hnegζ : IsPrimitiveRoot (-ζ) (2 * n) := by
    convert! IsPrimitiveRoot.orderOf (-ζ)
    rw [neg_eq_neg_one_mul, (Commute.all _ _).orderOf_mul_eq_mul_orderOf_of_coprime]
    · simp [hζ.eq_orderOf]
    · simp [← hζ.eq_orderOf, hno]

Goal state after:
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * n)
⊢ ∃ r, x = (-ζ) ^ r
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: n : ℕ
⊢ unitsMap ⋯ = MonoidHom.id (ZMod n)ˣ

Tactic:
simp [unitsMap, castHom_self]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ζ : C
h : IsPrimitiveRoot ζ n
⊢ (zmodChar n ⋯).IsPrimitive

Tactic:
by
  apply zmod_char_primitive_of_eq_one_only_at_zero
  intro a ha
  rw [zmodChar_apply, ← pow_zero ζ] at ha
  exact (ZMod.val_eq_zero a).mp (IsPrimitiveRoot.pow_inj h (ZMod.val_lt a) (NeZero.pos _) ha)

Goal state after:
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p✝ : ℕ
inst✝⁴ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Fintype K
inst✝ : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ ↑n'
hpp' : p = p'
this : Fact (Nat.Prime p)
⊢ K ≃+* K'

Tactic:
letI : Algebra (ZMod p) K := ZMod.algebra _ _

Goal state after:
p✝ : ℕ
inst✝⁴ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Fintype K
inst✝ : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ ↑n'
hpp' : p = p'
this✝ : Fact (Nat.Prime p)
this : Algebra (ZMod p) K := ZMod.algebra K p
⊢ K ≃+* K'
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst✝ : Nontrivial R
a : ℤ
⊢ IsCoprime (↑n) a ↔ IsCoprime a ↑n

Tactic:
isCoprime_comm

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst✝ : Nontrivial R
a : ℤ
⊢ IsCoprime a ↑n ↔ IsCoprime a ↑n
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: case calc_2
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : DecidableEq R
a : R
⊢ a ∈ Finset.filter IsUnit Finset.univ ↔ a ∈ Finset.map { toFun := Units.val, inj' := ⋯ } Finset.univ

Tactic:
simp [IsUnit]

Goal state after:
Module: Mathlib.Order.Grade

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
s : Flag α
a : ↥s
h : IsMin a
b : α
hba : b ≤ ↑a
⊢ ↑a ≤ b

Tactic:
refine @h ⟨b, mem_iff_forall_le_or_ge.2 fun c hc ↦ ?_⟩ hba

Goal state after:
α : Type u_3
inst✝ : PartialOrder α
s : Flag α
a : ↥s
h : IsMin a
b : α
hba : b ≤ ↑a
c : α
hc : c ∈ s
⊢ b ≤ c ∨ c ≤ b
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case refine_1
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := ψ₈char 1
⊢ (ψ₈.char 1 ^ 4) ^ 2 = 1

Tactic:
rw [← pow_mul, ← map_nsmul_eq_pow ψ₈.char, ψ₈.prim.zmod_char_eq_one_iff]
      decide

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
hst : ¬s ⊆ t
⊢ s ⊆ u → ¬u ⊆ t

Tactic:
exact fun hsu hut ↦ hst (hsu.trans hut)

Goal state after:
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 ι
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 : ℝ := ↑(#s)
hk' : 0 ≤ 1 - k * p
t : A i
⊢ f (X t) ^ (1 - k * p) * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) (X t) ^ p =
    (∫⋯∫⁻_{i}, f ∂μ) (X t) ^ p * (f (X t) ^ (1 - k * p) * ∏ j ∈ s, (∫⋯∫⁻_{j}, f ∂μ) (X t) ^ p)

Tactic:
prod_insert hi

Goal state after:
ι : 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 : ℝ := ↑(#s)
hk' : 0 ≤ 1 - k * p
t : A i
⊢ f (X t) ^ (1 - k * p) * ((∫⋯∫⁻_{i}, f ∂μ) (X t) ^ p * ∏ j ∈ s, (∫⋯∫⁻_{j}, f ∂μ) (X t) ^ p) =
    (∫⋯∫⁻_{i}, f ∂μ) (X t) ^ p * (f (X t) ^ (1 - k * p) * ∏ j ∈ s, (∫⋯∫⁻_{j}, f ∂μ) (X t) ^ p)
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 ι
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 : ℝ := ↑(#s)
hk' : 0 ≤ 1 - k * p
t : A i
⊢ f (X t) ^ (1 - k * p) * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) (X t) ^ p =
    (∫⋯∫⁻_{i}, f ∂μ) (X t) ^ p * (f (X t) ^ (1 - k * p) * ∏ j ∈ s, (∫⋯∫⁻_{j}, f ∂μ) (X t) ^ p)

Tactic:
simp_rw [prod_insert hi]

Goal state after:
ι : 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 : ℝ := ↑(#s)
hk' : 0 ≤ 1 - k * p
t : A i
⊢ f (X t) ^ (1 - k * p) * ((∫⋯∫⁻_{i}, f ∂μ) (X t) ^ p * ∏ j ∈ s, (∫⋯∫⁻_{j}, f ∂μ) (X t) ^ p) =
    (∫⋯∫⁻_{i}, f ∂μ) (X t) ^ p * (f (X t) ^ (1 - k * p) * ∏ j ∈ s, (∫⋯∫⁻_{j}, f ∂μ) (X t) ^ p)
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✝ : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫‖
⊢ IsUnit f

Tactic:
rw [isUnit_iff_bijective, bijective_iff_dense_range_and_antilipschitz]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖⟪f x, x⟫‖
⊢ (↑f).range.topologicalClosure = ⊤ ∧ ∃ c, AntilipschitzWith c ⇑f
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✝ : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
⊢ p.IsPositive ↔ IsSelfAdjoint p

Tactic:
by
  rw [← isPositive_toLinearMap_iff, IsIdempotentElem.isPositive_iff_isSymmetric hp.toLinearMap]
  exact isSelfAdjoint_iff_isSymmetric.symm

Goal state after:
Module: Mathlib.Topology.Algebra.Module.LinearPMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : f.graph.topologicalClosure = f'.graph
⊢ g.IsClosable

Tactic:
have : g.graph.topologicalClosure ≤ f'.graph := by
    rw [← hf]
    exact Submodule.topologicalClosure_mono (le_graph_of_le hfg)

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : f.graph.topologicalClosure = f'.graph
this : g.graph.topologicalClosure ≤ f'.graph
⊢ g.IsClosable
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 x = -birkhoffSum f g n x

Tactic:
simp [birkhoffSum]

Goal state after:
Module: Mathlib.Dynamics.BirkhoffSum.Basic

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝ : AddCommGroup G
f : α → α
g g' : α → G
n : ℕ
x : α
⊢ birkhoffSum f (g - g') n x = birkhoffSum f g n x - birkhoffSum f g' n x

Tactic:
simp [birkhoffSum]

Goal state after:
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 : α → α
x : α
h : IsFixedPt f x
g : α → M
n : ℕ
hn : ↑n ≠ 0
⊢ (↑n)⁻¹ • birkhoffSum f g n x = g x

Tactic:
h.birkhoffSum_eq,

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 : α → α
x : α
h : IsFixedPt f x
g : α → M
n : ℕ
hn : ↑n ≠ 0
⊢ (↑n)⁻¹ • n • g x = g x
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: 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
h0p : p ≠ 0
h1p : ↑p ≠ 1
h3p : ↑p - 1 ≠ 0
h2q : 1 / ↑n' - 1 / q = 1 / ↑p'
γ : ℝ≥0 := NNReal.mk (↑p * (↑n - 1) / (↑n - ↑p)) ⋯
h0γ : ↑γ = ↑p * (↑n - 1) / (↑n - ↑p)
⊢ ↑n < ↑p * ↑n

Tactic:
lt_mul_iff_one_lt_left

Goal state after:
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
h0p : p ≠ 0
h1p : ↑p ≠ 1
h3p : ↑p - 1 ≠ 0
h2q : 1 / ↑n' - 1 / q = 1 / ↑p'
γ : ℝ≥0 := NNReal.mk (↑p * (↑n - 1) / (↑n - ↑p)) ⋯
h0γ : ↑γ = ↑p * (↑n - 1) / (↑n - ↑p)
⊢ 1 < ↑p

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
h0p : p ≠ 0
h1p : ↑p ≠ 1
h3p : ↑p - 1 ≠ 0
h2q : 1 / ↑n' - 1 / q = 1 / ↑p'
γ : ℝ≥0 := NNReal.mk (↑p * (↑n - 1) / (↑n - ↑p)) ⋯
h0γ : ↑γ = ↑p * (↑n - 1) / (↑n - ↑p)
⊢ 0 < ↑n
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
n : ℕ
⊢ 0 < T.singularValues n ↔ n < finrank 𝕜 ↥T.range

Tactic:
rw [singularValues_pos_iff_ne_zero, ← Finsupp.mem_support_iff, support_singularValues,
    Finset.mem_range]

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
⊢ finrank 𝕜 ↥T.range ∉ T.singularValues.support

Tactic:
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
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x x' : E
y y' : F
⊢ edist (x ⊗ₜ[𝕜] y) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖ₑ * ‖y‖ₑ + ‖x'‖ₑ * ‖y'‖ₑ

Tactic:
grw [edist_eq_enorm_sub, enorm_sub_le]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x x' : E
y y' : F
⊢ ‖x ⊗ₜ[𝕜] y‖ₑ + ‖x' ⊗ₜ[𝕜] y'‖ₑ ≤ ‖x‖ₑ * ‖y‖ₑ + ‖x'‖ₑ * ‖y'‖ₑ
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : 𝕜 ⊗[𝕜] E
x✝¹ : 𝕜
x✝ : E
⊢ ∀ (x : 𝕜) (y : E),
    inner 𝕜 ((TensorProduct.lid 𝕜 E) (x✝¹ ⊗ₜ[𝕜] x✝)) ((TensorProduct.lid 𝕜 E) (x ⊗ₜ[𝕜] y)) =
      inner 𝕜 (x✝¹ ⊗ₜ[𝕜] x✝) (x ⊗ₜ[𝕜] y)

Tactic:
by simp [inner_smul_left, inner_smul_right, mul_assoc]

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
x : X
hxs : x ∈ s
hxt : ¬infEDist x t = 0
⊢ x ∈ ⋃ n, S n

Tactic:
rcases ENNReal.exists_inv_nat_lt hxt with ⟨n, hn⟩

Goal state after:
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
x : X
hxs : x ∈ s
hxt : ¬infEDist x t = 0
n : ℕ
hn : (↑n)⁻¹ < infEDist x t
⊢ x ∈ ⋃ n, S n