mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Convex.Set

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
X : ι → Type u_7
inst✝ : (i : ι) → ConvexSpace R (X i)
s : Set ι
t : (i : ι) → Set (X i)
ht : ∀ i ∈ s, IsConvexSet R (t i)
w : StdSimplex R ((i : ι) → X i)
hw : ↑w.weights.support ⊆ s.pi t
i : ι
hi : i ∈ s
⊢ (fun x ↦ x i) '' ↑w.weights.support ⊆ t i

Tactic:
hw,

Goal state after:
ι : Type u_1
R : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
X : ι → Type u_7
inst✝ : (i : ι) → ConvexSpace R (X i)
s : Set ι
t : (i : ι) → Set (X i)
ht : ∀ i ∈ s, IsConvexSet R (t i)
w : StdSimplex R ((i : ι) → X i)
hw : ↑w.weights.support ⊆ s.pi t
i : ι
hi : i ∈ s
⊢ (fun x ↦ x i) '' s.pi t ⊆ t i
Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion

Goal state before:
pp: case ht₁
𝕜 : Type ?u.4
E : Type ?u.12
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : DecidableEq E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep : AffineIndependent 𝕜 Subtype.val
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
⊢ s ⊆ s ∪ t

Tactic:
exact Finset.subset_union_left

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: ι : Sort u_1
V : Type u
G H : SimpleGraph V
a b c u v w : V
e : Sym2 V
x y : SimpleGraph V
⊢ x \ y = x ⊓ yᶜ

Tactic:
ext v w
    refine ⟨fun h => ⟨h.1, ⟨?_, h.2⟩⟩, fun h => ⟨h.1, h.2.2⟩⟩
    rintro rfl
    exact x.irrefl h.1

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

Goal state before:
pp: case neg
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_card : ↑(finrank 𝕜 E) + 1 ≤ ENat.card ι
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I = finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
h : ¬Infinite ι
⊢ ∃ J, I ⊆ J ∧ #J = finrank 𝕜 E + 1

Tactic:
have : Finite ι := Finite.of_not_infinite h

Goal state after:
case neg
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_card : ↑(finrank 𝕜 E) + 1 ≤ ENat.card ι
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I = finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
h : ¬Infinite ι
this : Finite ι
⊢ ∃ J, I ⊆ J ∧ #J = finrank 𝕜 E + 1
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: ι : Sort u_1
V : Type u
G H : SimpleGraph V
a b c u v w : V
e : Sym2 V
inst✝ : Nontrivial V
h : ⊥ = ⊤
⊢ ∀ (a b : V), a = b

Tactic:
by simpa only [← adj_inj, funext_iff, bot_adj,
    top_adj, ne_eq, eq_iff_iff, false_iff, not_not] using h

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

Goal state before:
pp: case neg
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_card : ↑(finrank 𝕜 E) + 1 ≤ ENat.card ι
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I = finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
h : ¬Infinite ι
this✝ : Finite ι
this : Fintype ι
⊢ finrank 𝕜 E + 1 ≤ Fintype.card ι

Tactic:
simp only [ENat.card_eq_coe_fintype_card] at h_card

Goal state after:
case neg
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I = finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
I : Finset ι
hI_card : #I ≤ finrank 𝕜 E + 1
h : ¬Infinite ι
this✝ : Finite ι
this : Fintype ι
h_card : ↑(finrank 𝕜 E) + 1 ≤ ↑(Fintype.card ι)
⊢ finrank 𝕜 E + 1 ≤ Fintype.card ι
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
ι : Sort u_2
inst✝ : Nonempty ι
f : ι → SimpleGraph V
⊢ (⨅ i, f i).edgeSet = ⋂ i, (f i).edgeSet

Tactic:
by
  ext ⟨x, y⟩
  have ⟨i⟩ := ‹Nonempty ι›
  simpa using (· i |>.ne)

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
a b : V
h : ¬G.Adj a b
hn : a ≠ b
⊢ G.incidenceSet a ∩ G.incidenceSet b = ∅

Tactic:
simp_rw [Set.eq_empty_iff_forall_notMem, Set.mem_inter_iff, not_and]

Goal state after:
V : Type u
G : SimpleGraph V
a b : V
h : ¬G.Adj a b
hn : a ≠ b
⊢ ∀ x ∈ G.incidenceSet a, x ∉ G.incidenceSet b
Module: Mathlib.Analysis.Convex.StoneSeparation

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
w : Fin 3 → 𝕜 := ⋯
z : Fin 3 → E := ⋯
hw₀ : ∀ (i : Fin 3), 0 ≤ w i
⊢ ∑ i, w i = az * av * bu + (bz * au * bv + au * av)

pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
w : Fin 3 → 𝕜 := ⋯
z : Fin 3 → E := ⋯
hw₀ : ∀ (i : Fin 3), 0 ≤ w i
⊢ az * av * bu + (bz * au * bv + au * av) = az * av + bz * au

Tactic:
· simp [w, Fin.sum_univ_succ]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
w : Fin 3 → 𝕜 := ⋯
z : Fin 3 → E := ⋯
hw₀ : ∀ (i : Fin 3), 0 ≤ w i
⊢ az * av * bu + (bz * au * bv + au * av) = az * av + bz * au
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ ↑s
this : Nonempty ↥s
⊢ IsConnected {y | s.SSameSide x y}

Tactic:
setOfPred_sSameSide_eq_image2 hx hp,

Goal state after:
V : Type u_2
P : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
x : P
hx : x ∉ s
p : P
hp : p ∈ ↑s
this : Nonempty ↥s
⊢ IsConnected (Set.image2 (fun t q ↦ t • (x -ᵥ p) +ᵥ q) (Set.Ioi 0) ↑s)
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✝¹ : 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)
hs : SignType.sign (w₁ i) = SignType.sign (w₂ i)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
j : Fin (n + 1)
hj : j ≠ i
hj' : s.points j ∈ affineSpan R (Set.range (s.faceOpposite i).points)
w₃ : Fin (n + 1) → R := w₂ - w₂ i • (w₁ i)⁻¹ • (w₁ - Pi.single j 1)
⊢ ∑ k, w₃ k = 1

Tactic:
simp [w₃, hw₂, ← Finset.mul_sum, hw₁]

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

Goal state before:
pp: V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
s : Set V
x y : V
hx : x ∉ (convexHull ℝ) s
hy : y ∈ (convexHull ℝ) s
hxy : IsVisible ℝ ((convexHull ℝ) s) x y
⊢ y ∈ (convexHull ℝ) {z | z ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x z}

Tactic:
obtain ⟨ι, _, w, a, hw₀, hw₁, ha, rfl⟩ := mem_convexHull_iff_exists_fintype.1 hy

Goal state after:
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
s : Set V
x : V
hx : x ∉ (convexHull ℝ) s
ι : Type
w✝ : Fintype ι
w : ι → ℝ
a : ι → V
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i, w i = 1
ha : ∀ (i : ι), a i ∈ s
hy : ∑ i, w i • a i ∈ (convexHull ℝ) s
hxy : IsVisible ℝ ((convexHull ℝ) s) x (∑ i, w i • a i)
⊢ ∑ i, w i • a i ∈ (convexHull ℝ) {z | z ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x z}
Module: Mathlib.MeasureTheory.Function.Holder

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst✝³ : NormedRing 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : MulActionWithZero 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ ‖f • g‖ ≤ ‖f‖ * ‖g‖

Tactic:
simp only [Lp.norm_def, ← ENNReal.toReal_mul]
  refine ENNReal.toReal_mono (by finiteness) ?_
  rw [eLpNorm_congr_ae (coeFn_lpSMul f g)]
  exact eLpNorm_smul_le_mul_eLpNorm (Lp.aestronglyMeasurable g) (Lp.aestronglyMeasurable f)

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✝¹ : 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)
⊢ (affineSpan R (Set.range (s.faceOpposite i).points)).WOppSide ((Finset.affineCombination R Finset.univ s.points) w₁)
      ((Finset.affineCombination R Finset.univ s.points) w₂) ↔
    SignType.sign (w₁ i) = -SignType.sign (w₂ i) ∨ w₁ i = 0 ∨ w₂ i = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · by_cases h0 : w₁ i = 0
    · simp [h0]
    by_cases h0' : w₂ i = 0
    · simp [h0']
    exact .inl ((s.sOppSide_affineSpan_faceOpposite_iff hw₁ hw₂).1 ⟨h,
      (s.affineCombination_mem_affineSpan_faceOpposite_iff hw₁).not.2 h0,
      (s.affineCombination_mem_affineSpan_faceOpposite_iff hw₂).not.2 h0'⟩).1
  · by_cases h0 : w₁ i = 0
    · exact wOppSide_of_left_mem _ ((s.affineCombination_mem_affineSpan_faceOpposite_iff hw₁).2 h0)
    · by_cases h0' : w₂ i = 0
      · exact wOppSide_of_right_mem _
          ((s.affineCombination_mem_affineSpan_faceOpposite_iff hw₂).2 h0')
      simp only [h0, h0', or_self, or_false] at h
      rcases Ne.lt_or_gt h0 with h' | h'
      · rw [sign_neg h', neg_inj, eq_comm, sign_eq_one_iff] at h
        exact (s.sOppSide_affineSpan_faceOpposite_of_pos_of_neg hw₂ hw₁ h h').symm.wOppSide
      · rw [sign_pos h', eq_comm, neg_eq_iff_eq_neg, sign_eq_neg_one_iff] at h
        exact (s.sOppSide_affineSpan_faceOpposite_of_pos_of_neg hw₁ hw₂ h' h).wOppSide

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)
t : ℝ
ht : t ∈ Ioc 0 1
⊢ f t = ENNReal.ofReal ((t ^ (-r⁻¹) - 1) ^ finrank ℝ E) * mB

Tactic:
refine μ.addHaar_closedBall (0 : E) ?_
      rw [sub_nonneg]
      exact Real.one_le_rpow_of_pos_of_le_one_of_nonpos ht.1 ht.2 (by simp [hr.le])

Goal state after:
Module: Mathlib.Analysis.Distribution.TestFunction

Goal state before:
pp: 𝕜 : Type u_1
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
n k : ℕ∞
inst✝¹ : Algebra ℝ 𝕜
inst✝ : IsScalarTower ℝ 𝕜 F
v₁ v₂ : E
x✝ : 𝓓^{n}(Ω, F)
a✝ : E
⊢ ((lineDerivCLM 𝕜 (v₁ + v₂)) x✝) a✝ = ((lineDerivCLM 𝕜 v₁ + lineDerivCLM 𝕜 v₂) x✝) a✝

Tactic:
simp [-lineDerivCLM_apply, lineDerivCLM_eq_fderivCLM]

Goal state after:
Module: Mathlib.Analysis.Distribution.TestFunction

Goal state before:
pp: 𝕜 : Type u_1
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
n k : ℕ∞
inst✝¹ : Algebra ℝ 𝕜
inst✝ : IsScalarTower ℝ 𝕜 F
c : ℝ
v : E
x✝ : 𝓓^{n}(Ω, F)
a✝ : E
⊢ ((lineDerivCLM 𝕜 (c • v)) x✝) a✝ = ((c • lineDerivCLM 𝕜 v) x✝) a✝

Tactic:
simp [-lineDerivCLM_apply, lineDerivCLM_eq_fderivCLM]

Goal state after:
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r ((↑N - r) * Real.log 2 / Real.log (3 / 2)) ≤ ↑k
hk₁ : r ≤ ↑k
hk₂ : Real.log 2 * (↑N - r) ≤ Real.log (3 / 2) * ↑k
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
this : ContDiffAt ℝ (↑n) (fun x ↦ x ^ r) x
hx' : 1 / 2 < x
hx'' : 0 < x
h✝ : r - ↑n < 0
h : 0 < ↑n - r
⊢ Real.exp (Real.log (3 / 2) * ↑k) ≤ (3 / 2) ^ k

Tactic:
← Real.rpow_natCast,

Goal state after:
H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r ((↑N - r) * Real.log 2 / Real.log (3 / 2)) ≤ ↑k
hk₁ : r ≤ ↑k
hk₂ : Real.log 2 * (↑N - r) ≤ Real.log (3 / 2) * ↑k
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
this : ContDiffAt ℝ (↑n) (fun x ↦ x ^ r) x
hx' : 1 / 2 < x
hx'' : 0 < x
h✝ : r - ↑n < 0
h : 0 < ↑n - r
⊢ Real.exp (Real.log (3 / 2) * ↑k) ≤ (3 / 2) ^ ↑k
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : 1 ≤ x
⊢ x ^ k * f = x ^ (-↑l) * (x ^ (k + l) * f)

Tactic:
← Real.rpow_natCast,

Goal state after:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : 1 ≤ x
⊢ x ^ ↑k * f = x ^ (-↑l) * (x ^ (k + l) * f)
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : 1 ≤ x
⊢ x ^ ↑k * f = x ^ (-↑l) * (x ^ (k + l) * f)

Tactic:
← Real.rpow_natCast,

Goal state after:
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : 1 ≤ x
⊢ x ^ ↑k * f = x ^ (-↑l) * (x ^ ↑(k + l) * f)
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case top
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
⊢ ∃ k, eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-↑k)) ∞ μ < ∞

Tactic:
exact ⟨0, eLpNormEssSup_lt_top_of_ae_bound (C := 1) (by simp)⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
S : End 𝕜 X
hS_not_surj : ¬Function.Surjective ⇑S
hS_anti : Topology.IsClosedEmbedding ⇑S
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
V : ℕ → Submodule 𝕜 X := fun n ↦ (LinearMap.iterateRange S) n
hV_succ : ∀ (n : ℕ), V (n + 1) = Submodule.map S (V n)
hV_closed : ∀ (n : ℕ), IsClosed ↑(V n)
n : ℕ
h₁ : IsClosed ↑(Submodule.comap (V n).subtype (V (n + 1)))
h₂ : ∃ x, x ∉ Submodule.comap (V n).subtype (V (n + 1))
⊢ ∃ x ∈ V n, 1 ≤ ‖x‖ ∧ ‖x‖ ≤ R ∧ ∀ y ∈ V (n + 1), 1 ≤ ‖x - y‖

Tactic:
obtain ⟨⟨x, hx⟩, hxn, hxy⟩ := riesz_lemma_of_norm_lt hc hR h₁ h₂

Goal state after:
𝕜 : Type u_1
X : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
S : End 𝕜 X
hS_not_surj : ¬Function.Surjective ⇑S
hS_anti : Topology.IsClosedEmbedding ⇑S
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
V : ℕ → Submodule 𝕜 X := fun n ↦ (LinearMap.iterateRange S) n
hV_succ : ∀ (n : ℕ), V (n + 1) = Submodule.map S (V n)
hV_closed : ∀ (n : ℕ), IsClosed ↑(V n)
n : ℕ
h₁ : IsClosed ↑(Submodule.comap (V n).subtype (V (n + 1)))
h₂ : ∃ x, x ∉ Submodule.comap (V n).subtype (V (n + 1))
x : X
hx : x ∈ V n
hxn : ‖⟨x, hx⟩‖ ≤ R
hxy : ∀ y ∈ Submodule.comap (V n).subtype (V (n + 1)), 1 ≤ ‖⟨x, hx⟩ - y‖
⊢ ∃ x ∈ V n, 1 ≤ ‖x‖ ∧ ‖x‖ ≤ R ∧ ∀ y ∈ V (n + 1), 1 ≤ ‖x - y‖
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:
simp_rw [← List.ofFn_inj, ← sort_roots_charpoly_eq_eigenvalues₀, h]

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

Goal state before:
pp: n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : C(↑(spectrum ℝ A), ℝ)
⊢ ((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary)
      (diagonal (RCLike.ofReal ∘ ⇑(star f) ∘ fun i ↦ ⟨hA.eigenvalues i, ⋯⟩)) =
    star
      (((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary)
        (diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨hA.eigenvalues i, ⋯⟩)))

Tactic:
simp only [star_trivial, ← map_star, star_eq_conjTranspose, diagonal_conjTranspose, Pi.star_def,
      Function.comp_apply, RCLike.star_def, RCLike.conj_ofReal]
    rfl

Goal state after:
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
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
i : Fin n
⊢ HasEigenvector T (↑((hT.unsortedEigenvalues hn ∘ ⇑(Tuple.sort (hT.unsortedEigenvalues hn)) ∘ ⇑Fin.revPerm) i))
    (((DirectSum.IsInternal.subordinateOrthonormalBasis hn ⋯ ⋯).reindex
        (Equiv.symm (Tuple.sort (hT.unsortedEigenvalues hn) * Fin.revPerm)))
      i)

Tactic:
OrthonormalBasis.reindex_apply

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
i : Fin n
⊢ HasEigenvector T (↑((hT.unsortedEigenvalues hn ∘ ⇑(Tuple.sort (hT.unsortedEigenvalues hn)) ∘ ⇑Fin.revPerm) i))
    ((DirectSum.IsInternal.subordinateOrthonormalBasis hn ⋯ ⋯)
      ((Equiv.symm (Tuple.sort (hT.unsortedEigenvalues hn) * Fin.revPerm)).symm i))
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
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ RCLike.re ⟪x, T x⟫
v : E
hv₁ : v ∈ (genEigenspace T ↑μ) 1
hv₂ : v ≠ 0
hpos : 0 < ‖v‖ ^ 2
⊢ 0 ≤ μ

Tactic:
simp only [mem_genEigenspace_one] at hv₁

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ RCLike.re ⟪x, T x⟫
v : E
hv₂ : v ≠ 0
hpos : 0 < ‖v‖ ^ 2
hv₁ : T v = ↑μ • v
⊢ 0 ≤ μ
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
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 < RCLike.re ⟪x, T x⟫
v : E
hv₁ : v ∈ (genEigenspace T ↑μ) 1
hv₂ : v ≠ 0
hpos : 0 < ‖v‖ ^ 2
⊢ 0 < μ

Tactic:
simp only [mem_genEigenspace_one] at hv₁

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 < RCLike.re ⟪x, T x⟫
v : E
hv₂ : v ≠ 0
hpos : 0 < ‖v‖ ^ 2
hv₁ : T v = ↑μ • v
⊢ 0 < μ
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
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 < RCLike.re ⟪x, T x⟫
⊢ 0 < μ

Tactic:
obtain ⟨v, hv₁, hv₂⟩ := hμ.exists_hasEigenvector
  have hpos : (0 : ℝ) < ‖v‖ ^ 2 := by simpa only [sq_pos_iff, norm_ne_zero_iff] using hv₂
  simp only [mem_genEigenspace_one] at hv₁
  have : RCLike.re ⟪v, T v⟫ = μ * ‖v‖ ^ 2 :=
    mod_cast congr_arg RCLike.re (inner_product_apply_eigenvector hv₁)
  exact (mul_pos_iff_of_pos_right hpos).mp (this ▸ hnn v)

Goal state after:
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
n : ℕ∞
K : Compacts E
m : MeasurableSpace E
inst✝¹⁰ : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝⁹ : NormedAddCommGroup F₁
inst✝⁸ : NormedSpace 𝕜 F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace 𝕜 F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace 𝕜 F₃
inst✝² : SMulCommClass ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
f : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K) μ
⊢ ‖(integralAgainstBilinLM B μ φ) f‖ ≤
    (∫ (x : E) in ↑K, ‖φ x‖ ∂μ) * ‖B‖ * (ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0) f

Tactic:
have h : ∀ᵐ x ∂(μ.restrict K), ‖B (f x) (φ x)‖ ≤ ‖φ x‖ * ‖B‖ * N[𝕜]_{K, n, 0} f := by
      filter_upwards [] with x
      grw [ContinuousLinearMap.le_opNorm, ContinuousLinearMap.le_opNorm, norm_apply_le_seminorm 𝕜,
        mul_comm, mul_assoc]
    rw [integralAgainstBilinLM_eq_setIntegral hφ]
    apply le_trans (norm_integral_le_of_norm_le ((hφ.norm.mul_const _).mul_const _) h)
    rw [integral_mul_const, integral_mul_const]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
l : β →₀ 𝕜
hl : (Finsupp.linearCombination 𝕜 ↑b) l = 0
⊢ ∀ (a : β), l a = 0 a

Tactic:
simpa [l.linearCombination_apply, Finsupp.sum, b.ortho, Pi.single_apply] using
    fun i ↦ congr_arg (b.coord i) hl

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
β : Type u_3
b : UnconditionalSchauderBasis β 𝕜 X
inst✝ : CompleteSpace X
x : X
A₀ : Finset β
hA₀ : ∀ (t : Finset β), Disjoint t A₀ → ‖∑ i ∈ t, (b.coord i) x • ↑b i‖ < 1
A : Finset β
⊢ ∑ i ∈ A, (b.coord i) x • ↑b i = ∑ x_1 ∈ A \ A₀ ∪ A ∩ A₀, (b.coord x_1) x • ↑b x_1

Tactic:
Finset.sdiff_union_inter

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
β : Type u_3
b : UnconditionalSchauderBasis β 𝕜 X
inst✝ : CompleteSpace X
x : X
A₀ : Finset β
hA₀ : ∀ (t : Finset β), Disjoint t A₀ → ‖∑ i ∈ t, (b.coord i) x • ↑b i‖ < 1
A : Finset β
⊢ ∑ i ∈ A, (b.coord i) x • ↑b i = ∑ x_1 ∈ A, (b.coord x_1) x • ↑b x_1