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

Goal state before:
pp: case refine_2
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✝² : IsDomain A
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑n
x✝ : n ≠ 0
this✝ : NeZero ↑n
this : NeZero ↑n
μ : CyclotomicField n K
hμ : IsPrimitiveRoot μ n
⊢ IsPrimitiveRoot ⟨μ, ⋯⟩ n

Tactic:
← IsPrimitiveRoot.coe_submonoidClass_iff,

Goal state after:
case refine_2
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✝² : IsDomain A
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑n
x✝ : n ≠ 0
this✝ : NeZero ↑n
this : NeZero ↑n
μ : CyclotomicField n K
hμ : IsPrimitiveRoot μ n
⊢ IsPrimitiveRoot (↑⟨μ, ⋯⟩) n
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

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

Tactic:
rw [toCircle_apply, Circle.coe_exp]

Goal state after:
N : ℕ
inst✝ : NeZero N
j : ZMod N
⊢ cexp (2 * ↑π * I * ↑j.val / ↑N) = cexp (↑(2 * π * (↑j.val / ↑N)) * I)
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst✝ : NeZero n
ψ : DirichletCharacter R m
h : (changeLevel ⋯) χ = (changeLevel ⋯) ψ
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap ⋯).ker
⊢ χ ↑x = 1

Tactic:
obtain ⟨z, hz₁, hz₂⟩ : ∃ z : ℕ, z = x.val ∧ (z : ZMod m) = 1 := by
    suffices x.val.val ≡ 1 [MOD n.gcd m] by
      obtain ⟨z, hz₁, hz₂⟩ := Nat.chineseRemainder' this
      refine ⟨z, ?_, ?_⟩
      · simpa [← ZMod.natCast_eq_natCast_iff] using hz₁
      · rwa [← ZMod.natCast_eq_natCast_iff, Nat.cast_one] at hz₂
    rwa [MonoidHom.mem_ker, Units.ext_iff, ZMod.unitsMap_val, ← ZMod.natCast_val,
      Units.val_one, ← Nat.cast_one, ZMod.natCast_eq_natCast_iff] at hx

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst✝ : NeZero n
ψ : DirichletCharacter R m
h : (changeLevel ⋯) χ = (changeLevel ⋯) ψ
x : (ZMod n)ˣ
hx : x ∈ (ZMod.unitsMap ⋯).ker
z : ℕ
hz₁ : ↑z = ↑x
hz₂ : ↑z = 1
⊢ χ ↑x = 1
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
hψ : ψ.Odd
⊢ (toUnitHom ψ) (-1) = -1

Tactic:
rw [← Units.val_inj, MulChar.coe_toUnitHom]

Goal state after:
S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
hψ : ψ.Odd
⊢ ψ ↑(-1) = ↑(-1)
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
hψ : ψ.Even
⊢ (toUnitHom ψ) (-1) = 1

Tactic:
rw [← Units.val_inj, MulChar.coe_toUnitHom]

Goal state after:
S : Type u_2
inst✝ : CommRing S
m : ℕ
ψ : DirichletCharacter S m
hψ : ψ.Even
⊢ ψ ↑(-1) = ↑1
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : ψ.IsPrimitive
⊢ χ ^ (orderOf χ - 1) = χ⁻¹

Tactic:
refine (inv_eq_of_mul_eq_one_right ?_).symm

Goal state after:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : ψ.IsPrimitive
⊢ χ * χ ^ (orderOf χ - 1) = 1
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ
hp : 1 < p
⊢ ‖p‖ * ‖f x‖ ^ (p - 2) * ‖(innerSL ℝ) (f x) ∘SL fderiv ℝ f x‖ ≤ p * ‖f x‖ ^ (p - 1) * ‖fderiv ℝ f x‖

Tactic:
norm_eq_abs,

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ
hp : 1 < p
⊢ |p| * ‖f x‖ ^ (p - 2) * ‖(innerSL ℝ) (f x) ∘SL fderiv ℝ f x‖ ≤ p * ‖f x‖ ^ (p - 1) * ‖fderiv ℝ f x‖
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ
hp : 1 < p
⊢ ‖p‖ * ‖‖f x‖ ^ (p - 2)‖ * ‖(innerSL ℝ) (f x) ∘SL fderiv ℝ f x‖ ≤ p * ‖f x‖ ^ (p - 1) * ‖fderiv ℝ f x‖

Tactic:
simp_rw [norm_rpow_of_nonneg (norm_nonneg _), norm_norm, norm_eq_abs,
    abs_eq_self.mpr <| zero_le_one.trans hp.le, mul_assoc]

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ
hp : 1 < p
⊢ p * (‖f x‖ ^ (p - 2) * ‖(innerSL ℝ) (f x) ∘SL fderiv ℝ f x‖) ≤ p * (‖f x‖ ^ (p - 1) * ‖fderiv ℝ f x‖)
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
⊢ auxDFT (auxDFT Φ) = fun j ↦ ↑N • Φ (-j)

Tactic:
ext1 j

Goal state after:
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j : ZMod N
⊢ auxDFT (auxDFT Φ) j = ↑N • Φ (-j)
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ ‖p‖ * ‖x‖ ^ (p - 2) * ‖(innerSL ℝ) x‖ = p * ‖x‖ ^ (p - 1)

Tactic:
norm_eq_abs,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ |p| * ‖x‖ ^ (p - 2) * ‖(innerSL ℝ) x‖ = p * ‖x‖ ^ (p - 1)
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
⊢ auxDFT ((fun Φ k ↦ (↑N)⁻¹ • auxDFT Φ (-k)) Φ) = Φ

Tactic:
ext1 j

Goal state after:
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
j : ZMod N
⊢ auxDFT ((fun Φ k ↦ (↑N)⁻¹ • auxDFT Φ (-k)) Φ) j = Φ j
Module: Mathlib.Analysis.Hofer

Goal state before:
pp: X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
H : ∀ ε' > 0, ∀ (x' : X), ε' ≤ ε → d x' x ≤ 2 * ε → ε * ϕ x ≤ ε' * ϕ x' → ∃ y, d x' y ≤ ε' ∧ 2 * ϕ x' < ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / 2 ^ k * ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x'
⊢ False

Tactic:
replace H : ∀ k : ℕ, ∀ x', d x' x ≤ 2 * ε ∧ 2 ^ k * ϕ x ≤ ϕ x' →
      ∃ y, d x' y ≤ ε / 2 ^ k ∧ 2 * ϕ x' < ϕ y := by
    intro k x'
    have := H (ε / 2 ^ k) (by positivity) x' (div_le_self ε_pos.le <| one_le_pow₀ one_le_two)
    simpa [reformulation] using! this

Goal state after:
X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / 2 ^ k * ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x'
H : ∀ (k : ℕ) (x' : X), d x' x ≤ 2 * ε ∧ 2 ^ k * ϕ x ≤ ϕ x' → ∃ y, d x' y ≤ ε / 2 ^ k ∧ 2 * ϕ x' < ϕ y
⊢ False
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 ((↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e) ∘ₗ LinearMap.lTensor E (toSpanSingleton 𝕜 E (e.symm 1))) =
    ↑(TensorProduct.comm 𝕜 E 𝕜 ≪≫ₗ TensorProduct.lid 𝕜 E).symm

Tactic:
← toLinearEquiv_commIsometry,

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))) =
    ↑((commIsometry 𝕜 E 𝕜).toLinearEquiv ≪≫ₗ TensorProduct.lid 𝕜 E).symm
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 ↑(TensorProduct.comm 𝕜 E 𝕜 ≪≫ₗ TensorProduct.lid 𝕜 E).symm) (x ⊗ₜ[𝕜] One.one) = x

Tactic:
← toLinearEquiv_commIsometry,

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 ↑((commIsometry 𝕜 E 𝕜).toLinearEquiv ≪≫ₗ TensorProduct.lid 𝕜 E).symm) (x ⊗ₜ[𝕜] One.one) = 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 ↑(TensorProduct.lid 𝕜 E).symm) (r ⊗ₜ[𝕜] x) =
    (adjoint ↑(TensorProduct.comm 𝕜 E 𝕜 ≪≫ₗ TensorProduct.lid 𝕜 E).symm) (x ⊗ₜ[𝕜] r)

Tactic:
← toLinearEquiv_commIsometry,

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 ↑(TensorProduct.lid 𝕜 E).symm) (r ⊗ₜ[𝕜] x) =
    (adjoint ↑((commIsometry 𝕜 E 𝕜).toLinearEquiv ≪≫ₗ TensorProduct.lid 𝕜 E).symm) (x ⊗ₜ[𝕜] r)
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp : (↑(finrank ℝ E)).HolderConjugate p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂μ ≤ ↑C * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂μ) ^ p

Tactic:
have : finrank ℝ E = finrank ℝ (ι → ℝ) := by simp [hιcard]

Goal state after:
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp : (↑(finrank ℝ E)).HolderConjugate p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ p ∂μ ≤ ↑C * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂μ) ^ p
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ
hp✝ : (↑(finrank ℝ E)).HolderConjugate p
C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p
ι : Type := Fin (finrank ℝ E)
hιcard : #ι = finrank ℝ E
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this
hp : (↑#ι).HolderConjugate p
h0p : 0 ≤ p
c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)
hc : 0 < c
h2c : μ = c • Measure.map (⇑e.symm) volume
h3c : ↑c ≠ 0
⊢ lintegralPowLePowLIntegralFDerivConst μ p =
    μ.addHaarScalarFactor (Measure.map (⇑(ContinuousLinearEquiv.ofFinrankEq this).symm) volume) *
        ‖↑(ContinuousLinearEquiv.ofFinrankEq this).symm‖₊ ^ p *
      (μ.addHaarScalarFactor (Measure.map (⇑(ContinuousLinearEquiv.ofFinrankEq this).symm) volume) ^ p)⁻¹

Tactic:
lintegralPowLePowLIntegralFDerivConst

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

Goal state before:
pp: F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ≥0
hp : (↑(finrank ℝ E)).HolderConjugate p
h0p : 0 < ↑p
⊢ eLpNorm u (↑p) μ ^ ↑p ≤
    ↑(lintegralPowLePowLIntegralFDerivConst μ ↑p ^ ((↑p)⁻¹ * ↑p)) * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂μ) ^ ↑p

Tactic:
eLpNorm_nnreal_pow_eq_lintegral hp.symm.pos.ne',

Goal state after:
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
u : E → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p : ℝ≥0
hp : (↑(finrank ℝ E)).HolderConjugate p
h0p : 0 < ↑p
⊢ ∫⁻ (x : E), ‖u x‖ₑ ^ ↑p ∂μ ≤
    ↑(lintegralPowLePowLIntegralFDerivConst μ ↑p ^ ((↑p)⁻¹ * ↑p)) * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ∂μ) ^ ↑p
Module: Mathlib.Analysis.InnerProductSpace.LinearPMap

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
g : Submodule 𝕜 (E × F)
x : F × E
⊢ x ∈ g.adjoint ↔ ∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0

Tactic:
simp only [Submodule.adjoint, mem_map, mem_orthogonal, LinearEquiv.coe_coe,
    LinearEquiv.trans_apply, LinearEquiv.skewSwap_symm_apply, coe_symm_linearEquiv, Prod.exists,
    prod_inner_apply, ofLp_fst, ofLp_snd, forall_exists_index, and_imp, coe_linearEquiv]
  constructor
  · rintro ⟨y, h1, h2⟩ a b hab
    rw [← h2, WithLp.ofLp_fst, WithLp.ofLp_snd]
    specialize h1 (toLp 2 (b, -a)) a b hab rfl
    dsimp at h1
    simp only [inner_neg_left, ← sub_eq_add_neg] at h1
    exact h1
  · intro h
    refine ⟨toLp 2 x, ?_, rfl⟩
    intro u a b hab hu
    simp [← hu, ← sub_eq_add_neg, h a b hab]

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
i : ℕ
⊢ 0 ≤ T.singularValues i

Tactic:
rw [singularValues, Finsupp.embDomain_apply, Finsupp.ofSupportFinite_coe]
  split_ifs <;> positivity

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

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
h : f.ker = ⊥
⊢ ¬f.normDet = 0

Tactic:
let g : U ≃ₗ[𝕜] f.range := LinearEquiv.ofBijective f.rangeRestrict
      ⟨by simpa using ker_eq_bot.mp h, f.surjective_rangeRestrict⟩

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
h : f.ker = ⊥
g : U ≃ₗ[𝕜] ↥f.range := LinearEquiv.ofBijective f.rangeRestrict ⋯
⊢ ¬f.normDet = 0
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: case neg
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 V
this : FiniteDimensional 𝕜 V
hdet : ¬‖((toMatrix bu.toBasis bv.toBasis) f).det‖ = 0
h : IsUnit ((toMatrix bu.toBasis bv.toBasis) f).det
f' : U ≃ₗ[𝕜] V := LinearEquiv.ofIsUnitDet h
hf : f.range = ⊤
⊢ finrank 𝕜 U = finrank 𝕜 ↥⊤

Tactic:
simpa using f'.finrank_eq

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

Goal state before:
pp: case pos
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
b : OrthonormalBasis ι 𝕜 U
h : f.ker = ⊥
bv : OrthonormalBasis ι 𝕜 ↥f.range := orthonormalBasis_range h b
⊢ ↑(f.normDet ^ 2) =
    star (Matrix.of fun i j ↦ (bv.repr (f.rangeRestrict (b j))).ofLp i).det *
      (Matrix.of fun i j ↦ (bv.repr (f.rangeRestrict (b j))).ofLp i).det

Tactic:
rw [RCLike.star_def, RCLike.conj_mul, f.normDet_eq_norm_det_toMatrix_rangeRestrict b bv]

Goal state after:
case pos
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
b : OrthonormalBasis ι 𝕜 U
h : f.ker = ⊥
bv : OrthonormalBasis ι 𝕜 ↥f.range := orthonormalBasis_range h b
⊢ ↑(‖((toMatrix b.toBasis bv.toBasis) f.rangeRestrict).det‖ ^ 2) =
    ↑‖(Matrix.of fun i j ↦ (bv.repr (f.rangeRestrict (b j))).ofLp i).det‖ ^ 2
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case inr
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
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
d : ℝ
hd : 0 ≤ d
hC0 : 0 < C
hCd0 : ↑C ^ d ≠ 0
hCd : ↑C ^ d ≠ ∞
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (fun d ↦ ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
⊢ ⨅ t,
      ⨅ (_ : f '' s ⊆ ⋃ n, t n),
        ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ R), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d ≤
    ⨆ i,
      ⨆ (_ : 0 < i),
        ⨅ i_1,
          ⨅ (_ : s ⊆ ⋃ n, i_1 n),
            ⨅ (_ : ∀ (n : ℕ), ediam (i_1 n) ≤ i),
              ∑' (i : ℕ), ⨆ (_ : (i_1 i).Nonempty), ↑C ^ d * ediam (i_1 i) ^ (↑r * d)

Tactic:
rcases ENNReal.nhds_zero_basis_Iic.eventually_iff.1 (this.eventually (gt_mem_nhds hR)) with
      ⟨δ, δ0, H⟩

Goal state after:
case inr
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
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
d : ℝ
hd : 0 ≤ d
hC0 : 0 < C
hCd0 : ↑C ^ d ≠ 0
hCd : ↑C ^ d ≠ ∞
R : ℝ≥0∞
hR : 0 < R
this : Tendsto (fun d ↦ ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : ∀ ⦃x : ℝ≥0∞⦄, x ∈ Iic δ → ↑C * x ^ ↑r < R
⊢ ⨅ t,
      ⨅ (_ : f '' s ⊆ ⋃ n, t n),
        ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ R), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), ediam (t n) ^ d ≤
    ⨆ i,
      ⨆ (_ : 0 < i),
        ⨅ i_1,
          ⨅ (_ : s ⊆ ⋃ n, i_1 n),
            ⨅ (_ : ∀ (n : ℕ), ediam (i_1 n) ≤ i),
              ∑' (i : ℕ), ⨆ (_ : (i_1 i).Nonempty), ↑C ^ d * ediam (i_1 i) ^ (↑r * d)
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 ((algebraMap ℝ (H →L[𝕜] H)) c - f)

Tactic:
IsUnit.sub_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
c : ℝ
hc : c < 0
⊢ IsUnit (f - (algebraMap ℝ (H →L[𝕜] H)) c)
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:
← neg_pos

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
⊢ Integrable (𝓕 g) volume

Tactic:
have h2π : 2 * π ≠ 0 := by simp

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
h2π : 2 * π ≠ 0
⊢ Integrable (𝓕 g) volume
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: case zero
s✝ : ℂ
hs✝ : ∀ (m : ℕ), s✝ ≠ -↑m
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
hsre : 0 < s.re
this : IsOpen {s | 0 < s.re}
⊢ Gamma =ᶠ[𝓝 s] GammaIntegral

Tactic:
filter_upwards [this.mem_nhds hsre] with a using Gamma_eq_integral

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: s : ℂ
aux1 : -1 < (s - 1).re
hs : s = 0
⊢ s.re ≤ 0

Tactic:
rw [hs, zero_re]

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

Goal state before:
pp: case refine_2
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
x : ℝ
hx : x ∈ Ioi 0
e1 : Tendsto (BohrMollerup.logGammaSeq x) atTop (𝓝 ((log ∘ f) x - log (f 1)))
⊢ (log ∘ f) x = (log ∘ Γ) x

Tactic:
hf_one,

Goal state after:
case refine_2
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
x : ℝ
hx : x ∈ Ioi 0
e1 : Tendsto (BohrMollerup.logGammaSeq x) atTop (𝓝 ((log ∘ f) x - log 1))
⊢ (log ∘ f) x = (log ∘ Γ) x
Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set P
hs : s ∈ ⨆ v ∈ Metric.sphere 0 1, asymptoticNhds ℝ P v
p : P
⊢ s ∈ cobounded P

Tactic:
simp_rw [mem_iSup, asymptoticNhds_eq_smul_vadd _ p, vadd_pure] at hs

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set P
p : P
hs : ∀ i ∈ Metric.sphere 0 1, s ∈ map (fun x ↦ x +ᵥ p) (atTop • 𝓝 i)
⊢ s ∈ cobounded P
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ↑n ^ (s + 1) * ↑n ! / ((∏ x ∈ Finset.range n, (s + 1 + ↑x)) * (s + 1 + ↑n) * s) =
    ↑n * ↑n ^ s * ↑n ! / ((∏ k ∈ Finset.range n, (s + ↑(k + 1))) * (↑n + 1 + s) * s)

Tactic:
congr 3

Goal state after:
case e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ↑n ^ (s + 1) = ↑n * ↑n ^ s

case e_a.e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ∏ x ∈ Finset.range n, (s + 1 + ↑x) = ∏ k ∈ Finset.range n, (s + ↑(k + 1))

case e_a.e_a.e_a
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ s + 1 + ↑n = ↑n + 1 + s