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

Goal state before:
pp: case 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
⊢ ∃ x, x ↑p = 1 ∧ (changeLevel ⋯) x = χ

Tactic:
have hdvd : χ.conductor ∣ n / p ^ n.factorization p := by
      apply Nat.dvd_ordCompl_of_dvd_not_dvd χ.conductor_dvd_level
      simp [← hp.out.coprime_iff_not_dvd, ← Nat.isCoprime_iff_coprime,
        ← apply_ne_zero_iff (χ := χ.primitiveCharacter), h]
    refine ⟨changeLevel hdvd χ.primitiveCharacter, ?_, ?_⟩
    · rw [show (p : ZMod (n / p ^ n.factorization p))
          = ((p : ℤ) : ZMod (n / p ^ n.factorization p)) from (Int.cast_natCast p).symm,
        changeLevel_eq_cast_of_dvd' χ.primitiveCharacter hdvd (Nat.isCoprime_iff_coprime.mpr hcop),
        Int.cast_natCast]
      exact h
    · rw [← changeLevel_trans, changeLevel_primitiveCharacter]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : gaussSum χ ψ ^ 2 = χ (-1) * ↑(Fintype.card R)
this : gaussSum χ ψ ≠ 0
⊢ gaussSum χ ψ ^ (2 * (p ^ n / 2)) * gaussSum χ ψ = gaussSum χ ψ ^ p ^ n

Tactic:
← pow_succ,

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : gaussSum χ ψ ^ 2 = χ (-1) * ↑(Fintype.card R)
this : gaussSum χ ψ ≠ 0
⊢ gaussSum χ ψ ^ (2 * (p ^ n / 2) + 1) = gaussSum χ ψ ^ p ^ n
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ IsAtom s ↔ ∃ a, s = {a}

Tactic:
simp [← bot_covBy_iff, covBy_iff_exists_cons, eq_comm]

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
⊢ ⟪b -ᵥ c, a -ᵥ c⟫ = dist b c ^ 2 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0

Tactic:
inner_vsub_vsub_right_eq_dist_sq_left_iff,

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
⊢ ⟪b -ᵥ c, a -ᵥ b⟫ = 0 ↔ ⟪a -ᵥ b, b -ᵥ c⟫ = 0
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case hxy.e'_6.a
ι : 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 := update x i
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ↑(#s)
hk' : 0 ≤ 1 - k * p
j : ι
hj : j ∈ s
⊢ (∫⋯∫⁻_{i, j}, f ∂μ) x = (∫⋯∫⁻_{j}, ∫⋯∫⁻_{i}, f ∂μ ∂μ) x

Tactic:
rw [← lmarginal_union μ f hf]

Goal state after:
case hxy.e'_6.a
ι : 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 := update x i
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ↑(#s)
hk' : 0 ≤ 1 - k * p
j : ι
hj : j ∈ s
⊢ (∫⋯∫⁻_{i, j}, f ∂μ) x = (∫⋯∫⁻_{j} ∪ {i}, f ∂μ) x

case hxy.e'_6.a
ι : 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 := update x i
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ↑(#s)
hk' : 0 ≤ 1 - k * p
j : ι
hj : j ∈ s
⊢ Disjoint {j} {i}
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case e'_4
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
p : ℝ
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ ∫⋯∫⁻_sᶜ, f ∂μ = ∫⋯∫⁻_{i}, ∫⋯∫⁻_(insert i s)ᶜ, f ∂μ ∂μ

Tactic:
rw [← lmarginal_union μ f hf]

Goal state after:
case e'_4
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
p : ℝ
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ ∫⋯∫⁻_sᶜ, f ∂μ = ∫⋯∫⁻_{i} ∪ (insert i s)ᶜ, f ∂μ

case e'_4
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
p : ℝ
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ Disjoint {i} (insert i s)ᶜ
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,
      ((starRingEnd 𝕜) ↑√(⋯.eigenvalues ⋯ x) * ⟪(⋯.eigenvectorBasis ⋯) x, x✝⟫) •
        ↑√(⋯.eigenvalues ⋯ x) • (⋯.eigenvectorBasis ⋯) x

Tactic:
smul_smul,

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,
      ((starRingEnd 𝕜) ↑√(⋯.eigenvalues ⋯ x) * ⟪(⋯.eigenvectorBasis ⋯) x, x✝⟫ * ↑√(⋯.eigenvalues ⋯ x)) •
        (⋯.eigenvectorBasis ⋯) x
Module: Mathlib.Analysis.InnerProductSpace.LinearPMap

Goal state before:
pp: case mpr
𝕜 : 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
h : ∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0
⊢ ∀ (u : WithLp 2 (F × E)) (x_1 : E) (x_2 : F),
    (x_1, x_2) ∈ g → toLp 2 (x_2, -x_1) = u → ⟪u.fst, (toLp 2 x).fst⟫ + ⟪u.snd, (toLp 2 x).snd⟫ = 0

Tactic:
intro u

Goal state after:
case mpr
𝕜 : 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
h : ∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0
u : WithLp 2 (F × E)
⊢ ∀ (x_1 : E) (x_2 : F), (x_1, x_2) ∈ g → toLp 2 (x_2, -x_1) = u → ⟪u.fst, (toLp 2 x).fst⟫ + ⟪u.snd, (toLp 2 x).snd⟫ = 0
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 : ℕ
hi : finrank 𝕜 E ≤ i
⊢ i ∉ Set.range ⇑Fin.valEmbedding

Tactic:
simp [hi]

Goal state after:
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
ι₁ : Type u_6
ι₂ : Type u_7
b₁ : Basis ι₁ 𝕜 E
b₂ : Basis ι₂ 𝕜 F
hb₁ : Orthonormal 𝕜 ⇑b₁
hb₂ : Orthonormal 𝕜 ⇑b₂
⊢ Orthonormal 𝕜 ⇑(b₁.tensorProduct b₂)

Tactic:
by
  convert! hb₁.tmul hb₂
  exact b₁.tensorProduct_apply' b₂ _

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 = ⊥
g : U ≃ₗ[𝕜] ↥f.range := LinearEquiv.ofBijective f.rangeRestrict ⋯
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range := ⋯ ▸ stdOrthonormalBasis 𝕜 ↥f.range
this :
  ((toMatrix bv.toBasis bu.toBasis) (adjoint f.rangeRestrict)).det *
      ((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det ≠
    0
⊢ ¬((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det = 0

Tactic:
by
      simpa [toMatrix_adjoint, Matrix.det_conjTranspose] using this

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

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
K : ℝ≥0
f : X → Y
s : Set X
h : LipschitzOnWith K f s
⊢ dimH (f '' s) ≤ dimH s

Tactic:
simpa using h.holderOnWith.dimH_image_le zero_lt_one

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
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 V
⊢ f.normDet = ‖((toMatrix bu.toBasis bv.toBasis) f).det‖

Tactic:
have : FiniteDimensional 𝕜 V := bv.toBasis.finiteDimensional_of_finite
  by_cases! hrank : finrank 𝕜 U = finrank 𝕜 f.range
  · have h : f.range = ⊤ := by
      apply Submodule.eq_of_le_of_finrank_le le_top
      simp [finrank_eq_card_basis bv.toBasis, ← hrank, finrank_eq_card_basis bu.toBasis]
    let bv' : OrthonormalBasis ι 𝕜 f.range := bv.map (LinearIsometryEquiv.ofTop _ _ h).symm
    rw [f.normDet_eq_norm_det_toMatrix_rangeRestrict bu bv']
    rfl
  · symm
    rw [normDet_eq_zero_iff_rank_range_ne.mpr hrank.symm]
    contrapose hrank with hdet
    have h : IsUnit ((f.toMatrix bu.toBasis bv.toBasis).det) := by
      simpa using hdet
    let f' := LinearEquiv.ofIsUnitDet h
    have hf : f.range = ⊤ := f'.range
    rw [hf]
    simpa using f'.finrank_eq

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

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
⊢ (boundedBy fun s ↦ extend (fun s x ↦ m (ediam s)) (f '' s)) = boundedBy (extend fun s x ↦ m (ediam s))

pp: X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
⊢ Monotone m → Monotone fun s ↦ extend (fun s x ↦ m (ediam s)) ↑s

Tactic:
· congr with s : 1
    apply extend_congr <;> simp [hf.ediam_image]

Goal state after:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
⊢ Monotone m → Monotone fun s ↦ extend (fun s x ↦ m (ediam s)) ↑s
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
f : U →ₗ[𝕜] V
c : 𝕜
hc : ¬c = 0
h : ¬f.ker = ⊥
⊢ (c • f).normDet = ‖c‖ ^ finrank 𝕜 U * f.normDet

Tactic:
have h' : (c • f).ker ≠ ⊥ := by simpa [f.ker_smul _ hc] using h

Goal state after:
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
f : U →ₗ[𝕜] V
c : 𝕜
hc : ¬c = 0
h : ¬f.ker = ⊥
h' : (c • f).ker ≠ ⊥
⊢ (c • f).normDet = ‖c‖ ^ finrank 𝕜 U * f.normDet
Module: Mathlib.Analysis.InnerProductSpace.OfNorm

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
hI : ¬I = 0
hI' : I * I = -1
v : E
⊢ ‖I • v‖ = ‖v‖

Tactic:
rw [norm_smul, norm_I_of_ne_zero hI, one_mul]

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

Goal state before:
pp: case neg
𝕜 : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : InnerProductSpace 𝕜 W
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
hf : f.ker = ⊥
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range
hgf : ¬(g ∘ₗ f).ker = ⊥
⊢ (g ∘ₗ f).normDet = (g.domRestrict f.range).normDet * f.normDet

Tactic:
have hg : (g.domRestrict f.range).ker ≠ ⊥ := by
        contrapose hf with hgf'
        rw [← LinearMap.ker_rangeRestrict, ← LinearMap.ker_comp_of_ker_eq_bot _ hgf']
        exact hgf

Goal state after:
case neg
𝕜 : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : InnerProductSpace 𝕜 W
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
hf : f.ker = ⊥
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range
hgf : ¬(g ∘ₗ f).ker = ⊥
hg : (g.domRestrict f.range).ker ≠ ⊥
⊢ (g ∘ₗ f).normDet = (g.domRestrict f.range).normDet * f.normDet
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)))
⊢ μH[↑(finrank ℝ U)] (⇑(g.symm.toLinearIsometry.toLinearMap ∘ₗ f.rangeRestrict) '' s) =
    ENNReal.ofReal f.normDet * μH[↑(finrank ℝ U)] s

Tactic:
addHaar_image_linearMap μH[finrank ℝ U],

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 |LinearMap.det (g.symm.toLinearIsometry.toLinearMap ∘ₗ f.rangeRestrict)| * μH[↑(finrank ℝ U)] s =
    ENNReal.ofReal f.normDet * μH[↑(finrank ℝ U)] s
Module: Mathlib.Analysis.InnerProductSpace.OfNorm

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
x y : E
hI' : I * I = -1
⊢ 4⁻¹ *
      (𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖ + I * 𝓚 ‖I • I • x + y‖ * 𝓚 ‖I • I • x + y‖ -
        I * 𝓚 ‖I • I • x - y‖ * 𝓚 ‖I • I • x - y‖) =
    4⁻¹ *
      (-I *
        (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ -
          I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖))

Tactic:
smul_smul,

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
x y : E
hI' : I * I = -1
⊢ 4⁻¹ *
      (𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖ + I * 𝓚 ‖(I * I) • x + y‖ * 𝓚 ‖(I * I) • x + y‖ -
        I * 𝓚 ‖(I * I) • x - y‖ * 𝓚 ‖(I * I) • x - y‖) =
    4⁻¹ *
      (-I *
        (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ -
          I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖))
Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace

Goal state before:
pp: H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
⊢ S.mulI.mulI = S

Tactic:
by
  ext x
  simp only [Submodule.carrier_eq_coe, coe_toSubmodule, SetLike.mem_coe]
  constructor
  · intro h
    rw [mem_mapEquiv_iff (scalarSMulCLE H UnitI), ← SetLike.forall_smul_mem_iff] at h
    simpa [← smul_assoc, Units.smul_def] using (h (-1 : ℝ))
  · intro h
    rw [← SetLike.forall_smul_mem_iff] at h
    simpa [← smul_assoc, Units.smul_def] using (h (-1 : ℝ))

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

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

Tactic:
by
  rw [SpectrumRestricts.nnreal_iff]
  intro c hc
  contrapose! hc
  rw [spectrum.notMem_iff, IsUnit.sub_iff, sub_eq_add_neg, ← map_neg]
  rw [← neg_pos] at hc
  set c := -c
  exact isUnit_of_forall_le_norm_inner_map _ (c := ⟨c, hc.le⟩) hc fun x ↦ calc
    ‖x‖ ^ 2 * c = re ⟪algebraMap ℝ (H →L[𝕜] H) c x, x⟫_𝕜 := by
      rw [Algebra.algebraMap_eq_smul_one, ← algebraMap_smul 𝕜 c (1 : (H →L[𝕜] H)), smul_apply,
        one_apply_eq_self, inner_smul_left, RCLike.algebraMap_eq_ofReal, conj_ofReal, re_ofReal_mul,
        inner_self_eq_norm_sq, mul_comm]
    _ ≤ re ⟪(f + (algebraMap ℝ (H →L[𝕜] H)) c) x, x⟫_𝕜 := by
      simpa only [add_apply, inner_add_left, map_add, le_add_iff_nonneg_left]
        using hf.re_inner_nonneg_left x
    _ ≤ ‖⟪(f + (algebraMap ℝ (H →L[𝕜] H)) c) x, x⟫_𝕜‖ := RCLike.re_le_norm _

Goal state after:
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:
by
  rw [e.isometry.map_hausdorffMeasure (Or.inr e.surjective), e.surjective.range_eq, restrict_univ]

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded

Goal state before:
pp: 𝕜 : 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✝ : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
U : Set F
hU : U ∈ 𝓝 0
V : Set E
hV : V ∈ 𝓝 0
h✝ : IsVonNBounded 𝕜' (⇑f '' V)
r : ℝ
hr : r > 0
h : ∀ (c : 𝕜'), r ≤ ‖c‖ → ⇑f '' V ⊆ c • U
⊢ ⇑f ⁻¹' U ∈ 𝓝 0

Tactic:
rcases NormedField.exists_lt_norm 𝕜 r with ⟨x, hx⟩

Goal state after:
𝕜 : 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✝ : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
U : Set F
hU : U ∈ 𝓝 0
V : Set E
hV : V ∈ 𝓝 0
h✝ : IsVonNBounded 𝕜' (⇑f '' V)
r : ℝ
hr : r > 0
h : ∀ (c : 𝕜'), r ≤ ‖c‖ → ⇑f '' V ⊆ c • U
x : 𝕜
hx : r < ‖x‖
⊢ ⇑f ⁻¹' U ∈ 𝓝 0
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)
x : E
⊢ o.volumeForm ![x, x] = 0

Tactic:
refine o.volumeForm.map_eq_zero_of_eq ![x, x] ?_ (?_ : (0 : Fin 2) ≠ 1)

Goal state after:
case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ ![x, x] 0 = ![x, x] 1

case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ 0 ≠ 1
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)
x y : E
h : ⟪x, y⟫ = 0
⊢ ∏ i, ‖![x, y] i‖ = ‖x‖ * ‖y‖

Tactic:
simp [Fin.prod_univ_succ]

Goal state after:
Module: Mathlib.Analysis.Matrix.LDL

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : WellFoundedLT n
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
i j : n
hij : ¬i = j
⊢ 0 = lowerInv hS i ⬝ᵥ S *ᵥ (lowerInv hS)ᴴᵀ j

Tactic:
rw [conjTranspose, transpose_map, transpose_transpose, dotProduct_mulVec,
      (LDL.lowerInv_orthogonal hS fun h : j = i => hij h.symm).symm, ← inner_conj_symm,
      mulVec_transpose, EuclideanSpace.inner_toLp_toLp, ← RCLike.star_def, ←
      star_dotProduct_star, star_star]

Goal state after:
case neg
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : WellFoundedLT n
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
i j : n
hij : ¬i = j
⊢ lowerInv hS i ᵥ* S ⬝ᵥ star (lowerInv hS j) = lowerInv hS i ᵥ* S ⬝ᵥ (lowerInv hS).map star j
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: ⊢ range rexp = Ioi 0

Tactic:
Real.range_exp

Goal state after:
⊢ Ioi 0 = Ioi 0
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
⊢ 1 • mellin f (s / ↑(-1)) = mellin f (-s)

Tactic:
one_smul,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
⊢ mellin f (s / ↑(-1)) = mellin f (-s)
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
f : ℂ → ℂ := fun z ↦ log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z ↦ (-z) ^ n * (1 + z)⁻¹
⊢ ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)

Tactic:
intro t ht

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
f' : ℂ → ℂ := fun z ↦ (-z) ^ n * (1 + z)⁻¹
t : ℝ
ht : t ∈ Set.Icc 0 1
⊢ HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
⊢ Γ (a * s + b * t) ≤ Γ s ^ a * Γ t ^ b

Tactic:
have hst : 0 < a * s + b * t := by positivity

Goal state after:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
⊢ Γ (a * s + b * t) ≤ Γ s ^ a * Γ t ^ b