mathlib-initiative/mathlib-tactics huggingface dataset:
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
w : V
hw : w ≠ 0
⊢ (starRingEnd ℝ) (1 / (2 * ‖w‖ ^ 2)) * id ‖w‖ ^ 2 = 1 / 2

Tactic:
id,

Goal state after:
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
w : V
hw : w ≠ 0
⊢ (starRingEnd ℝ) (1 / (2 * ‖w‖ ^ 2)) * ‖w‖ ^ 2 = 1 / 2
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case neg
n : ℕ
h : ¬Squarefree n
⊢ μ n ^ 2 = 0

Tactic:
simp only [moebius_eq_zero_of_not_squarefree h, zero_pow (show 2 ≠ 0 by simp)]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Periodic

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : AddCommGroup X
inst✝³ : ContinuousAdd X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : Summable fun n ↦ f.comp (ContinuousMap.addRight (n • p))
⊢ (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) (x + p) =
    (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) x

Tactic:
convert! congr_arg (fun f : C(X, Y) => f x) ((Equiv.addRight (1 : ℤ)).tsum_eq _) using 1

Goal state after:
case e'_2
X : Type u_1
Y : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : AddCommGroup X
inst✝³ : ContinuousAdd X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : Summable fun n ↦ f.comp (ContinuousMap.addRight (n • p))
⊢ (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) (x + p) =
    (∑' (c : ℤ), f.comp (ContinuousMap.addRight ((Equiv.addRight 1) c • p))) x
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : (X ^ n - C 1).Monic
⊢ (X ^ n - C 1).roots.card = (X ^ n - C 1).natDegree

Tactic:
@natDegree_X_pow_sub_C R _ _ n 1,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hmonic : (X ^ n - C 1).Monic
⊢ (X ^ n - C 1).roots.card = n
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
α : R
hα : α ^ n = a
hα' : ¬α = 0
⊢ (nthRoots n a).Nodup

Tactic:
nthRoots_eq h hα,

Goal state after:
case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
α : R
hα : α ^ n = a
hα' : ¬α = 0
⊢ (Multiset.map (fun x ↦ ζ ^ x * α) (Multiset.range n)).Nodup
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: case pos
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
hfi : Integrable f volume
⊢ Tendsto (fun w ↦ ∫ (v : V), 𝐞 (-⟪v, w⟫) • f v) (cocompact V) (𝓝 0)

Tactic:
refine Metric.tendsto_nhds.mpr fun ε hε => ?_

Goal state after:
case pos
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
hfi : Integrable f volume
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (x : V) in cocompact V, dist (∫ (v : V), 𝐞 (-⟪v, x⟫) • f v) 0 < ε
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case mpr
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
a : ℕ
ha : x ∈ primitiveRoots a R
d : ℕ
hd : n = a * d
hazero : 0 < a
⊢ x ^ n = 1

Tactic:
mem_primitiveRoots hazero

Goal state after:
case mpr
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
a : ℕ
ha : IsPrimitiveRoot x a
d : ℕ
hd : n = a * d
hazero : 0 < a
⊢ x ^ n = 1
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
P : ℤ[X] := minpoly ℤ μ
⊢ n.totient ≤ (minpoly ℤ μ).natDegree

Tactic:
let P_K : K[X] := map (Int.castRingHom K) P

Goal state after:
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
P : ℤ[X] := minpoly ℤ μ
P_K : K[X] := map (Int.castRingHom K) P
⊢ n.totient ≤ (minpoly ℤ μ).natDegree
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : (cyclotomic n K).IsRoot μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
⊢ False

Tactic:
have ho : 0 < orderOf μ := (isOfFinOrder_iff_pow_eq_one.2 <| ⟨n, hnpos, hμn⟩).orderOf_pos

Goal state after:
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : (cyclotomic n K).IsRoot μ
hμn : μ ^ n = 1
hnμ : ¬IsPrimitiveRoot μ n
ho : 0 < orderOf μ
⊢ False
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
f : S ≃ₐ[R] S
⊢ μ ^ (↑((autToPow R hμ) f)).val = f μ

Tactic:
by
  rw [IsPrimitiveRoot.coe_autToPow_apply]
  generalize_proofs h
  refine (?_ : ((hμ.toRootsOfUnity : Sˣ) : S) ^ _ = _).trans h.choose_spec.symm
  rw [← rootsOfUnity.coe_pow, ← rootsOfUnity.coe_pow]
  congr 2
  rw [pow_eq_pow_iff_modEq, ZMod.val_natCast]
  conv => enter [2, 2]; rw [hμ.eq_orderOf]
  rw [← Subgroup.orderOf_coe, ← orderOf_units]
  exact Nat.mod_modEq _ _

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this✝ : NeZero n
this : (expand ℤ p) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ
⊢ (expand R p) (cyclotomic n R) = cyclotomic (n * p) R

Tactic:
rw [← map_cyclotomic_int, ← map_expand, this, map_cyclotomic_int]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case h.inl.hb.inr.inl
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
hx : 0 < x + 1
hi : 2 ≠ 1 ∧ 2 ∣ n ∧ 2 < n
⊢ 0 ≤ eval x (cyclotomic 2 R)

pp: case h.inl.hb.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
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hx : 0 < x + 1
hk : i ≠ 2
⊢ 0 ≤ eval x (cyclotomic i R)

Tactic:
· simpa only [eval_X, eval_one, cyclotomic_two, eval_add] using hx.le

Goal state after:
case h.inl.hb.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
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hx : 0 < x + 1
hk : i ≠ 2
⊢ 0 ≤ eval x (cyclotomic i R)
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case inl
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : GCDMonoid.lcm l n = n * r
ineq : φ n * φ r ≤ φ (GCDMonoid.lcm l n)
rpos : 0 < r
key : r = 1
⊢ l ∣ 2 * n

Tactic:
rw [key, mul_one] at hr

Goal state after:
case inl
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
ζ : K
l : ℕ
hζ : IsPrimitiveRoot ζ l
hl✝ : l ≠ 0
hl : NeZero l
hroot : IsPrimitiveRoot (zeta n ℚ K) n
r : ℕ
hr : GCDMonoid.lcm l n = n
ineq : φ n * φ r ≤ φ (GCDMonoid.lcm l n)
rpos : 0 < r
key : r = 1
⊢ l ∣ 2 * n
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
⊢ (q - 1) ^ φ n < eval q (cyclotomic n ℝ)

Tactic:
have hn : 0 < n := pos_of_gt hn'

Goal state after:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
⊢ (q - 1) ^ φ n < eval q (cyclotomic n ℝ)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
⊢ eval q (cyclotomic n ℝ) < (q + 1) ^ φ n

Tactic:
have hn : 0 < n := pos_of_gt hn'

Goal state after:
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
⊢ eval q (cyclotomic n ℝ) < (q + 1) ^ φ n
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommMonoid R'
inst✝ : Finite R
e : AddChar R R'
r x : R
h : x * r = 0
h' : ¬x = 0
⊢ ¬(e.mulShift r).mulShift x ≠ 1

Tactic:
simp only [mulShift_mulShift, mul_comm r, h, mulShift_zero, not_ne_iff]

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

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

Tactic:
toCircle,

Goal state after:
N : ℕ
inst✝ : NeZero N
j : ℤ
⊢ ↑((toCircle_addChar.compAddMonoidHom toAddCircle) ↑j) = cexp (2 * ↑π * I * ↑j / ↑N)
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ (n / 2)

Tactic:
← Nat.div_add_mod n 4

Goal state after:
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ ((4 * (n / 4) + n % 4) / 2)
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
hd : d ∣ n
h : (ZMod.unitsMap hd).ker ≤ (toUnitHom χ).ker
⊢ χ.FactorsThrough d

Tactic:
let E := MonoidHom.liftOfSurjective _ (ZMod.unitsMap_surjective hd) ⟨_, h⟩

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
inst✝ : NeZero n
hd : d ∣ n
h : (ZMod.unitsMap hd).ker ≤ (toUnitHom χ).ker
E : (ZMod d)ˣ →* Rˣ := ((ZMod.unitsMap hd).liftOfSurjective ⋯) ⟨toUnitHom χ, h⟩
⊢ χ.FactorsThrough d
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
f : R' →+* R''
⊢ ringHomComp 1 f = 1

Tactic:
ext1
  simp only [MulChar.ringHomComp_apply, MulChar.one_apply_coe, map_one]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:

Tactic:
∑ a, (1 : MulChar R R') a * ψ a + 1
  _ = ∑ a ∈ {0}ᶜ, (1 : MulChar R R') a * ψ a + 1 := by
    simp [← ({0} : Finset R).sum_compl_add_sum]
  _ = ∑ a ∈ {0}ᶜ, ψ a + ψ 0 := by
    congr! <;> aesop (add simp MulChar.one_apply)
  _ = 0 := by
    rw [← AddChar.sum_eq_zero_of_ne_one hψ, ← Finset.sum_compl_add_sum (s := {0})]
    simp

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

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
inst✝² : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
inst✝¹ : NeZero n
inst✝ : Nontrivial R
p : ℕ
hp : Fact (Nat.Prime p)
this : NeZero (n / p ^ n.factorization p)
hcop : p.Coprime (n / p ^ n.factorization p)
h : χ.primitiveCharacter ↑p = 1
hdvd : χ.conductor ∣ n / p ^ n.factorization p
⊢ (changeLevel ⋯) ((changeLevel hdvd) χ.primitiveCharacter) = χ

Tactic:
· rw [← changeLevel_trans, changeLevel_primitiveCharacter]

Goal state after:
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₁ * (t₂ * ⟪b -ᵥ a, c -ᵥ a⟫)) + (|t₂| * ‖c -ᵥ a‖) ^ 2 =
    t₁ ^ 2 * dist a b ^ 2 + t₂ ^ 2 * dist a c ^ 2

Tactic:
h_inner

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₂ * 0)) + (|t₂| * ‖c -ᵥ a‖) ^ 2 =
    t₁ ^ 2 * dist a b ^ 2 + t₂ ^ 2 * dist a c ^ 2
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
A : Type u_3
inst✝³ : Ring A
inst✝² : Module 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
e : E ≃ₗ[𝕜] A
⊢ adjoint (LinearMap.rTensor E (toSpanSingleton 𝕜 E (e.symm 1))) ∘ₗ adjoint (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e) =
    (TensorProduct.mk 𝕜 𝕜 E) 1

Tactic:
← adjoint_comp,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : FiniteDimensional 𝕜 E
A : Type u_3
inst✝³ : Ring A
inst✝² : Module 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
e : E ≃ₗ[𝕜] A
⊢ adjoint ((↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e) ∘ₗ LinearMap.rTensor E (toSpanSingleton 𝕜 E (e.symm 1))) =
    (TensorProduct.mk 𝕜 𝕜 E) 1
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
A : Type u_3
inst✝³ : Ring A
inst✝² : Module 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
e : E ≃ₗ[𝕜] A
⊢ adjoint (LinearMap.lTensor E (toSpanSingleton 𝕜 E (e.symm 1))) ∘ₗ adjoint (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e) =
    (TensorProduct.mk 𝕜 E 𝕜).flip 1

Tactic:
← adjoint_comp,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : FiniteDimensional 𝕜 E
A : Type u_3
inst✝³ : Ring A
inst✝² : Module 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
e : E ≃ₗ[𝕜] A
⊢ adjoint ((↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e) ∘ₗ LinearMap.lTensor E (toSpanSingleton 𝕜 E (e.symm 1))) =
    (TensorProduct.mk 𝕜 E 𝕜).flip 1
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
⊢ (adjoint comul ∘ₗ adjoint (LinearMap.rTensor E comul)) (x ⊗ₜ[𝕜] y ⊗ₜ[𝕜] z) =
    (adjoint comul) (x ⊗ₜ[𝕜] (adjoint comul) (y ⊗ₜ[𝕜] z))

Tactic:
← adjoint_comp,

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 (LinearMap.rTensor E comul ∘ₗ comul)) (x ⊗ₜ[𝕜] y ⊗ₜ[𝕜] z) =
    (adjoint comul) (x ⊗ₜ[𝕜] (adjoint comul) (y ⊗ₜ[𝕜] z))
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 : E
⊢ (adjoint comul ∘ₗ adjoint (LinearMap.rTensor E counit)) (One.one ⊗ₜ[𝕜] x) = x

Tactic:
← adjoint_comp,

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 : E
⊢ (adjoint (LinearMap.rTensor E counit ∘ₗ comul)) (One.one ⊗ₜ[𝕜] x) = x
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 : E
⊢ (adjoint comul ∘ₗ adjoint (LinearMap.lTensor E counit)) (x ⊗ₜ[𝕜] One.one) = x

Tactic:
← adjoint_comp,

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 : E
⊢ (adjoint (LinearMap.lTensor E counit ∘ₗ comul)) (x ⊗ₜ[𝕜] One.one) = x
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: E' : Type u_4
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℂ E'
T : E' →ₗ[ℂ] E'
⊢ ((∀ (v : E'), ↑(⟪T v, v⟫_ℂ).re = ⟪T v, v⟫_ℂ) ∧ ∀ (x : E'), 0 ≤ (⟪T x, x⟫_ℂ).re) ↔
    (∀ (x : E'), ↑(⟪T x, x⟫_ℂ).re = ⟪T x, x⟫_ℂ) ∧ ∀ (x : E'), 0 ≤ (⟪T x, x⟫_ℂ).re

Tactic:
Complex.coe_algebraMap

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 : 𝕜
⊢ (adjoint counit) (x * y) = (adjoint comul ∘ₗ adjoint (map counit counit)) (x ⊗ₜ[𝕜] y)

Tactic:
← adjoint_comp,

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 : 𝕜
⊢ (adjoint counit) (x * y) = (adjoint (map counit counit ∘ₗ comul)) (x ⊗ₜ[𝕜] y)
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsPositive
c : 𝕜
hc : 0 ≤ c
hc' : (starRingEnd 𝕜) c = c
x : E
⊢ 0 ≤ re ⟪(c • T) x, x⟫

Tactic:
smul_apply,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsPositive
c : 𝕜
hc : 0 ≤ c
hc' : (starRingEnd 𝕜) c = c
x : E
⊢ 0 ≤ re ⟪c • T x, x⟫
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
r : 𝕜
x : E
⊢ (adjoint comul ∘ₗ adjoint (LinearMap.rTensor E counit)) (r ⊗ₜ[𝕜] x) =
    (adjoint comul ∘ₗ adjoint (LinearMap.lTensor E counit)) (x ⊗ₜ[𝕜] r)

Tactic:
← adjoint_comp,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
r : 𝕜
x : E
⊢ (adjoint (LinearMap.rTensor E counit ∘ₗ comul)) (r ⊗ₜ[𝕜] x) =
    (adjoint (LinearMap.lTensor E counit ∘ₗ comul)) (x ⊗ₜ[𝕜] r)
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
r : 𝕜
x : E
⊢ r • x = (adjoint comul ∘ₗ adjoint (LinearMap.rTensor E counit)) (r ⊗ₜ[𝕜] x)

Tactic:
← adjoint_comp,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
r : 𝕜
x : E
⊢ r • x = (adjoint (LinearMap.rTensor E counit ∘ₗ comul)) (r ⊗ₜ[𝕜] x)
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: ι : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
p : ℝ
hp : (↑#ι).HolderConjugate p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ ↑#ι - 1
x : ι → ℝ
i : ι
a✝ : i ∈ Finset.univ
⊢ ContDiff ℝ 1 (update x i)

Tactic:
by convert! contDiff_update 1 x i

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

Goal state before:
pp: ι : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
p : ℝ
hp : (↑#ι).HolderConjugate p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ ↑#ι - 1
x : ι → ℝ
i : ι
a✝ : i ∈ Finset.univ
⊢ HasCompactSupport (u ∘ update x i)

Tactic:
· exact h2u.comp_isClosedEmbedding (isClosedEmbedding_update x i)

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
U V : Submodule 𝕜 E
inst✝¹ : U.HasOrthogonalProjection
inst✝ : V.HasOrthogonalProjection
⊢ U.starProjection = V.starProjection ↔ U = V

Tactic:
simp only [le_antisymm_iff, ← starProjection_le_starProjection_iff]

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
⊢ IsLowerSet ↑T.singularValues.support

Tactic:
intro a b hl ha

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
a b : ℕ
hl : b ≤ a
ha : a ∈ ↑T.singularValues.support
⊢ b ∈ ↑T.singularValues.support
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:
singularValues_pos_iff_ne_zero,

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
n : ℕ
⊢ T.singularValues n ≠ 0 ↔ n < finrank 𝕜 ↥T.range
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
i : ℕ
⊢ finrank 𝕜 ↥(range 0) ≤ i

Tactic:
range_zero

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
i : ℕ
⊢ finrank 𝕜 ↥⊥ ≤ i
Module: Mathlib.Analysis.InnerProductSpace.SingularValues

Goal state before:
pp: case mpr
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
h : T = 0
⊢ T.singularValues = 0

Tactic:
· exact h ▸ singularValues_zero

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
f₁ f₂ : E →L[𝕜] F
g : G →L[𝕜] H
x✝ : E ⊗[𝕜] G
⊢ (mapL (f₁ + f₂) g) x✝ = (mapL f₁ g + mapL f₂ g) x✝

Tactic:
simp [map_add_left]

Goal state after: