mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
⊢ x ∈ s ∨ y ∈ s → s.WSameSide x y ∧ s.WOppSide x y

Tactic:
rintro (h | h)

Goal state after:
case mpr.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
h : x ∈ s
⊢ s.WSameSide x y ∧ s.WOppSide x y

case mpr.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
h : y ∈ s
⊢ s.WSameSide x y ∧ s.WOppSide x y
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
h : s.SSameSide x y
ho : s.WOppSide x y
hy : y ∈ s
⊢ False

Tactic:
exact h.2.2 hy

Goal state after:
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ y ∈ {y | s.WSameSide x y} ↔ y ∈ Set.image2 (fun t q ↦ t • (x -ᵥ p) +ᵥ q) (Set.Ici 0) ↑s

Tactic:
simp_rw [Set.mem_ofPred, Set.mem_image2, Set.mem_Ici]

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x p : P
hx : x ∉ s
hp : p ∈ s
y : P
⊢ s.WSameSide x y ↔ ∃ a, 0 ≤ a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y
Module: Mathlib.Analysis.Distribution.Distribution

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
Ω : Opens E
F : Type u_2
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : TopologicalSpace F
n k : ℕ∞
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
v₁ v₂ : E
T : 𝓓'^{k}(Ω, F)
f : 𝓓^{n}(Ω, ℝ)
⊢ ((lineDerivCLM (v₁ + v₂)) T) f = ((lineDerivCLM v₁ + lineDerivCLM v₂) T) f

Tactic:
simp [lineDerivCLM_apply, TestFunction.lineDerivCLM_add, neg_add, -neg_add_rev]

Goal state after:
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: case refine_2.inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : ∑ j, w₁ j = 1
hw₂ : ∑ j, w₂ j = 1
i : Fin (n + 1)
x✝ : SignType.sign (w₁ i) = -SignType.sign (w₂ i) ∧ w₁ i ≠ 0
hs : w₂ i < 0
h0 : w₁ i ≠ 0
h' : 0 < w₁ i
⊢ (affineSpan R (Set.range (s.faceOpposite i).points)).SOppSide ((Finset.affineCombination R Finset.univ s.points) w₁)
    ((Finset.affineCombination R Finset.univ s.points) w₂)

Tactic:
exact s.sOppSide_affineSpan_faceOpposite_of_pos_of_neg hw₁ hw₂ h' hs

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω ↦ (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → μ {a | t ≤ (1 + ‖a‖) ^ (-r)} = μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t ↦ μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := μ (Metric.ball 0 1)
⊢ lintegral (volume.restrict (Ioi 0)) f < ∞

Tactic:
calc
    ∫⁻ t in Ioi 0, f t ≤ ∫⁻ t in Ioc 0 1 ∪ Ioi 1, f t := lintegral_mono_set Ioi_subset_Ioc_union_Ioi
    _ ≤ (∫⁻ t in Ioc 0 1, f t) + ∫⁻ t in Ioi 1, f t := lintegral_union_le _ _ _
    _ < ∞ := ENNReal.add_lt_top.2 ⟨?_, ?_⟩

Goal state after:
case calc_1
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω ↦ (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → μ {a | t ≤ (1 + ‖a‖) ^ (-r)} = μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t ↦ μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := μ (Metric.ball 0 1)
⊢ ∫⁻ (t : ℝ) in Ioc 0 1, f t < ∞

case calc_2
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω ↦ (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → μ {a | t ≤ (1 + ‖a‖) ^ (-r)} = μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t ↦ μ (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := μ (Metric.ball 0 1)
⊢ ∫⁻ (t : ℝ) in Ioi 1, f t < ∞
Module: Mathlib.Analysis.Distribution.TestFunction

Goal state before:
pp: case mk
𝕜 : Type u_1
𝕂 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace 𝕜 F
F' : Type u_5
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
g : 𝓓^{n}(Ω, F)
toFun✝ : E → F
contDiff'✝ : ContDiff ℝ (↑n) toFun✝
hasCompactSupport'✝ : HasCompactSupport toFun✝
tsupport_subset'✝ : tsupport toFun✝ ⊆ ↑Ω
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, contDiff' := contDiff'✝, hasCompactSupport' := hasCompactSupport'✝,
        tsupport_subset' := tsupport_subset'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, contDiff' := contDiff'✝, hasCompactSupport' := hasCompactSupport'✝,
      tsupport_subset' := tsupport_subset'✝ } =
    g

Tactic:
cases g

Goal state after:
case mk.mk
𝕜 : Type u_1
𝕂 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
Ω Ω₁ Ω₂ : Opens E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace 𝕜 F
F' : Type u_5
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedSpace 𝕜 F'
n n₁ n₂ k : ℕ∞
toFun✝¹ : E → F
contDiff'✝¹ : ContDiff ℝ (↑n) toFun✝¹
hasCompactSupport'✝¹ : HasCompactSupport toFun✝¹
tsupport_subset'✝¹ : tsupport toFun✝¹ ⊆ ↑Ω
toFun✝ : E → F
contDiff'✝ : ContDiff ℝ (↑n) toFun✝
hasCompactSupport'✝ : HasCompactSupport toFun✝
tsupport_subset'✝ : tsupport toFun✝ ⊆ ↑Ω
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝¹, contDiff' := contDiff'✝¹, hasCompactSupport' := hasCompactSupport'✝¹,
        tsupport_subset' := tsupport_subset'✝¹ } =
    (fun f ↦ f.toFun)
      { toFun := toFun✝, contDiff' := contDiff'✝, hasCompactSupport' := hasCompactSupport'✝,
        tsupport_subset' := tsupport_subset'✝ }
⊢ { toFun := toFun✝¹, contDiff' := contDiff'✝¹, hasCompactSupport' := hasCompactSupport'✝¹,
      tsupport_subset' := tsupport_subset'✝¹ } =
    { toFun := toFun✝, contDiff' := contDiff'✝, hasCompactSupport' := hasCompactSupport'✝,
      tsupport_subset' := tsupport_subset'✝ }
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case hg₁
D : Type u_4
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup D
inst✝ : NormedSpace ℝ D
g : E → F
f : D → E
hg : HasTemperateGrowth g
hf : HasTemperateGrowth f
⊢ ContDiffOn ℝ ∞ g Set.univ

Tactic:
contDiffOn_univ

Goal state after:
case hg₁
D : Type u_4
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup D
inst✝ : NormedSpace ℝ D
g : E → F
f : D → E
hg : HasTemperateGrowth g
hf : HasTemperateGrowth f
⊢ ContDiff ℝ ∞ g
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : Nontrivial E
hT' : (algebraMap ℝ 𝕜) ‖T‖ ∈ resolventSet 𝕜 T
hT'' : -(algebraMap ℝ 𝕜) ‖T‖ ∈ resolventSet 𝕜 T
⊢ ∃ ε > 0, ∀ (x : E), |T.rayleighQuotient x| ≤ ‖T‖ - ε

Tactic:
by
  obtain ⟨ε, hε0, hε⟩ := T.rayleighQuotient_le_of_norm_mem_resolventSet hT'
  obtain ⟨ε', hε'0, hε'⟩ := (-T).rayleighQuotient_le_of_norm_mem_resolventSet <| by
    simpa [resolventSet_neg]
  exact ⟨min ε ε', by grind, fun x ↦ by grind [rayleighQuotient_neg_apply, norm_neg]⟩

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

Goal state before:
pp: case pos
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
T : F →L[ℝ] F
hT : IsSelfAdjoint T
x₀ : F
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
a b : ℝ
h₁ : (a, b) ≠ 0
h₂ : a • x₀ + b • T x₀ = 0
hx₀ : x₀ = 0
⊢ T x₀ = T.rayleighQuotient x₀ • x₀

Tactic:
simp [hx₀]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ 0 < ‖x₀‖

Tactic:
simp [hx₀]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ 0 < ‖x₀‖

Tactic:
simp [hx₀]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Sort

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : f ∘ ⇑σ ≠ f ∘ ⇑(sort f)
⊢ ∃ i j, i < j ∧ (f ∘ ⇑σ) j < (f ∘ ⇑σ) i

Tactic:
contrapose! h
  exact comp_sort_eq_comp_iff_monotone.mpr (monotone_iff_forall_lt.mpr h)

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

Goal state before:
pp: case mpr
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A B : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
hB : B.IsHermitian
h : A.charpoly = B.charpoly
⊢ hA.eigenvalues = hB.eigenvalues

Tactic:
suffices hA.eigenvalues₀ = hB.eigenvalues₀ by unfold eigenvalues; rw [this]

Goal state after:
case mpr
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A B : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
hB : B.IsHermitian
h : A.charpoly = B.charpoly
⊢ hA.eigenvalues₀ = hB.eigenvalues₀
Module: Mathlib.Analysis.Matrix.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
| A.rank

Tactic:
rw [hA.spectral_theorem, conjStarAlgAut_apply, ← coe_star]

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
| (↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * ↑(star hA.eigenvectorUnitary)).rank
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
g : 𝓓^{n}_{K}(E, F)
toFun✝ : E → F
contDiff'✝ : ContDiff ℝ (↑n) toFun✝
zero_on_compl'✝ : EqOn toFun✝ 0 (↑K)ᶜ
h :
  (fun f ↦ f.toFun) { toFun := toFun✝, contDiff' := contDiff'✝, zero_on_compl' := zero_on_compl'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, contDiff' := contDiff'✝, zero_on_compl' := zero_on_compl'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedSpace 𝕜 F'
inst✝ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k : ℕ∞
K K₁ K₂ : Compacts E
toFun✝¹ : E → F
contDiff'✝¹ : ContDiff ℝ (↑n) toFun✝¹
zero_on_compl'✝¹ : EqOn toFun✝¹ 0 (↑K)ᶜ
toFun✝ : E → F
contDiff'✝ : ContDiff ℝ (↑n) toFun✝
zero_on_compl'✝ : EqOn toFun✝ 0 (↑K)ᶜ
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, contDiff' := contDiff'✝¹, zero_on_compl' := zero_on_compl'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, contDiff' := contDiff'✝, zero_on_compl' := zero_on_compl'✝ }
⊢ { toFun := toFun✝¹, contDiff' := contDiff'✝¹, zero_on_compl' := zero_on_compl'✝¹ } =
    { toFun := toFun✝, contDiff' := contDiff'✝, zero_on_compl' := zero_on_compl'✝ }
Module: Mathlib.Analysis.Matrix.PosDef

Goal state before:
pp: m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A M : Matrix n n 𝕜
hM : M.PosSemidef
x y : n → 𝕜
⊢ (starRingEnd 𝕜) (star y ⬝ᵥ M *ᵥ x) = M *ᵥ y ⬝ᵥ star x

Tactic:
star_dotProduct,

Goal state after:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A M : Matrix n n 𝕜
hM : M.PosSemidef
x y : n → 𝕜
⊢ (starRingEnd 𝕜) (star (star (M *ᵥ x) ⬝ᵥ y)) = M *ᵥ y ⬝ᵥ star x
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hT : T.IsSymmetric
hT' : (T.restrict ⋯).IsSymmetric
this : Subsingleton ↥(⨆ μ, eigenspace T μ)ᗮ
⊢ (⨆ μ, eigenspace T μ)ᗮ = ⊥

Tactic:
exact Submodule.eq_bot_of_subsingleton

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
x : ι →₀ 𝕜
hx : x ≠ 0
hAs : (A.submatrix Subtype.val Subtype.val).PosDef
hBs : (B.submatrix Subtype.val Subtype.val).PosDef
⊢ ((A ⊙ B).submatrix Subtype.val Subtype.val).PosDef

Tactic:
rw [submatrix_hadamard, posDef_iff_dotProduct_mulVec]

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
x : ι →₀ 𝕜
hx : x ≠ 0
hAs : (A.submatrix Subtype.val Subtype.val).PosDef
hBs : (B.submatrix Subtype.val Subtype.val).PosDef
⊢ (A.submatrix Subtype.val Subtype.val ⊙ B.submatrix Subtype.val Subtype.val).IsHermitian ∧
    ∀ ⦃x_1 : ↥x.support → 𝕜⦄,
      x_1 ≠ 0 → 0 < star x_1 ⬝ᵥ A.submatrix Subtype.val Subtype.val ⊙ B.submatrix Subtype.val Subtype.val *ᵥ x_1
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: case negSucc
A : Type u_2
inst✝¹⁰ : Ring A
inst✝⁹ : StarRing A
inst✝⁸ : TopologicalSpace A
inst✝⁷ : Algebra ℝ A
inst✝⁶ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : IsTopologicalRing A
inst✝¹ : T2Space A
inst✝ : StarModule ℝ A
n : ℕ
⊢ abs ↑(Int.negSucc n) = ↑|Int.negSucc n|

Tactic:
| negSucc n =>

Goal state after:
Module: Mathlib.MeasureTheory.Function.ContinuousMapDense

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst✝⁶] s
u_open : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hs : μ s ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst✝⁶] V
h'V : μ V < ∞
hV : μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : μ v < ∞
g : C(α, ℝ)
hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ
hgs : EqOn (⇑g) 1 s
hg_range : ∀ (x : α), g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖g x‖ = g x
gc_bd0 : ∀ (x : α), ‖g x • c‖ ≤ ‖c‖
x : α
⊢ ‖g x • c - s.indicator (fun _x ↦ c) x‖ ≤ ‖(v \ s).indicator (fun _x ↦ c) x‖

Tactic:
by_cases hv : x ∈ v

Goal state after:
case pos
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst✝⁶] s
u_open : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hs : μ s ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst✝⁶] V
h'V : μ V < ∞
hV : μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : μ v < ∞
g : C(α, ℝ)
hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ
hgs : EqOn (⇑g) 1 s
hg_range : ∀ (x : α), g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖g x‖ = g x
gc_bd0 : ∀ (x : α), ‖g x • c‖ ≤ ‖c‖
x : α
hv : x ∈ v
⊢ ‖g x • c - s.indicator (fun _x ↦ c) x‖ ≤ ‖(v \ s).indicator (fun _x ↦ c) x‖

case neg
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst✝⁶] s
u_open : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hs : μ s ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst✝⁶] V
h'V : μ V < ∞
hV : μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : μ v < ∞
g : C(α, ℝ)
hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ
hgs : EqOn (⇑g) 1 s
hg_range : ∀ (x : α), g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖g x‖ = g x
gc_bd0 : ∀ (x : α), ‖g x • c‖ ≤ ‖c‖
x : α
hv : x ∉ v
⊢ ‖g x • c - s.indicator (fun _x ↦ c) x‖ ≤ ‖(v \ s).indicator (fun _x ↦ c) x‖
Module: Mathlib.MeasureTheory.Function.ContinuousMapDense

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst✝⁶] s
u_open : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hs : μ s ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst✝⁶] V
h'V : μ V < ∞
hV : μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : μ v < ∞
g : C(α, ℝ)
hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ
hgs : EqOn (⇑g) 1 s
hg_range : ∀ (x : α), g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖g x‖ = g x
gc_bd0 : ∀ (x : α), ‖g x • c‖ ≤ ‖c‖
gc_bd : ∀ (x : α), ‖g x • c - s.indicator (fun _x ↦ c) x‖ ≤ ‖(v \ s).indicator (fun _x ↦ c) x‖
gc_support : (Function.support fun x ↦ g x • c) ⊆ v
⊢ ∃ f,
    Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧
      eLpNorm (fun x ↦ f x - s.indicator (fun _y ↦ c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ MemLp f p μ

Tactic:
have gc_mem : MemLp (fun x => g x • c) p μ := by
    refine MemLp.smul (memLp_top_const _) ?_ (p := p) (q := ∞)
    refine ⟨g.continuous.aestronglyMeasurable, ?_⟩
    have : eLpNorm (v.indicator fun _x => (1 : ℝ)) p μ < ⊤ :=
      (eLpNorm_indicator_const_le _ _).trans_lt <| by simp [lt_top_iff_ne_top, hμv.ne]
    refine (eLpNorm_mono fun x => ?_).trans_lt this
    by_cases hx : x ∈ v
    · simp only [hx, abs_of_nonneg (hg_range x).1, (hg_range x).2, Real.norm_eq_abs,
        indicator_of_mem, CStarRing.norm_one]
    · simp only [hgv hx, Pi.zero_apply, Real.norm_eq_abs, abs_zero, abs_nonneg]

Goal state after:
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst✝⁶] s
u_open : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hs : μ s ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst✝⁶] V
h'V : μ V < ∞
hV : μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : μ v < ∞
g : C(α, ℝ)
hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ
hgs : EqOn (⇑g) 1 s
hg_range : ∀ (x : α), g x ∈ Icc 0 1
g_norm : ∀ (x : α), ‖g x‖ = g x
gc_bd0 : ∀ (x : α), ‖g x • c‖ ≤ ‖c‖
gc_bd : ∀ (x : α), ‖g x • c - s.indicator (fun _x ↦ c) x‖ ≤ ‖(v \ s).indicator (fun _x ↦ c) x‖
gc_support : (Function.support fun x ↦ g x • c) ⊆ v
gc_mem : MemLp (fun x ↦ g x • c) p μ
⊢ ∃ f,
    Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f ∧
      eLpNorm (fun x ↦ f x - s.indicator (fun _y ↦ c) x) p μ ≤ ε ∧
        (∀ (x : α), ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ MemLp f p μ
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : ↥(lp G 2)
c : 𝕜
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
calc
        _ = ∑' i, ⟪c • f i, g i⟫ := ?_
        _ = ∑' i, conj c * ⟪f i, g i⟫ := by simp only [inner_smul_left]
        _ = conj c * ∑' i, ⟪f i, g i⟫ := tsum_mul_left
        _ = _ := ?_

Goal state after:
case calc_1
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : ↥(lp G 2)
c : 𝕜
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

case calc_2
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : ↥(lp G 2)
c : 𝕜
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
⊢ x ≠ y → ∃ f ∈ (fun f ↦ ⇑f) '' ↑fourierSubalgebra.toSubalgebra, f x ≠ f y

Tactic:
hxy

Goal state after:
T : ℝ
hT : Fact (0 < T)
x y : AddCircle T
hxy : x ≠ y
⊢ ∃ f ∈ (fun f ↦ ⇑f) '' ↑fourierSubalgebra.toSubalgebra, f x ≠ f y
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun x ↦ 𝕜) 2)
i : ι
this✝ : NormedSpace 𝕜 ↥(lp (fun _i ↦ 𝕜) 2) := inferInstance
this : lp.single 2 i (↑f i) = ↑f i • lp.single 2 i 1
⊢ lp.single 2 i (↑f i) = b.repr (↑b.repr.symm ((fun i ↦ lp.single 2 i (↑f i)) i))

Tactic:
LinearIsometryEquiv.coe_toContinuousLinearEquiv

Goal state after:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun x ↦ 𝕜) 2)
i : ι
this✝ : NormedSpace 𝕜 ↥(lp (fun _i ↦ 𝕜) 2) := inferInstance
this : lp.single 2 i (↑f i) = ↑f i • lp.single 2 i 1
⊢ lp.single 2 i (↑f i) = b.repr (b.repr.symm ((fun i ↦ lp.single 2 i (↑f i)) i))