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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : T2Space E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul ℝ E
inst✝⁴ : LocallyConvexSpace ℝ E
s : Set E
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : TopologicalSpace F
inst✝ : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
x : E
hx : x ∈ s
hw : f x ∈ extremePoints ℝ (⇑f '' s)
ht : IsCompact {x_1 | x_1 ∈ s ∧ f x_1 = f x}
ht₀ : {x_1 | x_1 ∈ s ∧ f x_1 = f x}.Nonempty
hyt :
  ∀ ⦃x₁ : E⦄,
    x₁ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} →
      ∀ ⦃x₂ : E⦄, x₂ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} → x ∈ openSegment ℝ x₁ x₂ → x₁ = x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
hxyz : x ∈ openSegment ℝ y z
⊢ y = x

Tactic:
have := by simpa using! image_openSegment _ f.toAffineMap y z

Goal state after:
E : Type u_1
F : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module ℝ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : T2Space E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul ℝ E
inst✝⁴ : LocallyConvexSpace ℝ E
s : Set E
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : TopologicalSpace F
inst✝ : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
x : E
hx : x ∈ s
hw : f x ∈ extremePoints ℝ (⇑f '' s)
ht : IsCompact {x_1 | x_1 ∈ s ∧ f x_1 = f x}
ht₀ : {x_1 | x_1 ∈ s ∧ f x_1 = f x}.Nonempty
hyt :
  ∀ ⦃x₁ : E⦄,
    x₁ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} →
      ∀ ⦃x₂ : E⦄, x₂ ∈ {x_1 | x_1 ∈ s ∧ f x_1 = f x} → x ∈ openSegment ℝ x₁ x₂ → x₁ = x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
hxyz : x ∈ openSegment ℝ y z
this : (fun a ↦ f a) '' openSegment ℝ y z = openSegment ℝ (f y) (f z)
⊢ y = x
Module: Mathlib.Geometry.Convex.ConvexSpace.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
I : Type u_6
inst✝³ : PartialOrder R
inst✝² : Semiring R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R M
J : I → Type u_9
s : StdSimplex R I
f : (i : I) → StdSimplex R (J i)
g : (i : I) → J i → M
⊢ (iConvexComb s fun i ↦ iConvexComb (f i) (g i)) =
    iConvexComb (iConvexComb s fun i ↦ map (fun x ↦ ⟨i, x⟩) (f i)) (Sigma.uncurry g)

Tactic:
by
  simp only [iConvexComb]
  rw [← map_map, ← sConvexComb_sConvexComb]
  congr 1
  simp [map_sConvexComb, map_map, Sigma.uncurry]

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

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_6
γ : Type u_7
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
⊢ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ {x | x ∈ s ∧ (g ∘ f) x ≤ c}

Tactic:
intro a

Goal state after:
𝕜 : Type u_4
E : Type u_5
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_6
γ : Type u_7
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a : 𝕜
⊢ ∀ ⦃b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ {x | x ∈ s ∧ (g ∘ f) x ≤ c}
Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq 𝕜
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
abstract : PreAbstractSimplicialComplex ι
x : ι →₀ 𝕜
hx : x ∈ ⋃ s ∈ (abstract.map fun i ↦ Finsupp.single i 1).faces, ↑s
⊢ x ∈ Set.range fun i ↦ Finsupp.single i 1

Tactic:
simp only [Set.mem_iUnion, Finset.mem_coe] at hx

Goal state after:
𝕜 : Type u_1
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq 𝕜
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
abstract : PreAbstractSimplicialComplex ι
x : ι →₀ 𝕜
hx : ∃ i, ∃ (_ : i ∈ (abstract.map fun i ↦ Finsupp.single i 1).faces), x ∈ i
⊢ x ∈ Set.range fun i ↦ Finsupp.single i 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
G : SimpleGraph V
v w : V
x✝ : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
right✝ : ¬G.Adj v w
⊢ ¬G.Adj w v

Tactic:
rwa [adj_comm]

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
G₁ G₂ : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype ↑G₁.edgeSet
inst✝ : Fintype ↑G₂.edgeSet
⊢ Fintype ↑(G₁ ⊓ G₂).edgeSet

Tactic:
edgeSet_inf

Goal state after:
ι : Sort u_1
V : Type u
G H : SimpleGraph V
a b c u v w : V
e : Sym2 V
G₁ G₂ : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype ↑G₁.edgeSet
inst✝ : Fintype ↑G₂.edgeSet
⊢ Fintype ↑(G₁.edgeSet ∩ G₂.edgeSet)
Module: Mathlib.Analysis.Convex.StrictConvexBetween

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : StrictConvexSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c : P
this : dist a b + dist b c = dist a c ↔ b -ᵥ a ∈ (fun x ↦ x -ᵥ a) '' affineSegment ℝ a c
⊢ dist a b + dist b c = dist a c ↔ Wbtw ℝ a b c

Tactic:
rwa [(vsub_left_injective _).mem_set_image] at this

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.SSameSide x y} ↔ y ∈ Set.image2 (fun t q ↦ t • (x -ᵥ p) +ᵥ q) (Set.Ioi 0) ↑s

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

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.SSameSide x y ↔ ∃ a, 0 < a ∧ ∃ b ∈ ↑s, a • (x -ᵥ p) +ᵥ b = y
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
h : (↑s).Nonempty
⊢ IsConnected {y | s.SSameSide x y}

Tactic:
obtain ⟨p, hp⟩ := h
  have : Nonempty s := ⟨⟨p, hp⟩⟩
  rw [setOfPred_sSameSide_eq_image2 hx hp, ← Set.image_prod]
  refine (isConnected_Ioi.prod (isConnected_iff_connectedSpace.2 ?_)).image _
    ((continuous_fst.smul continuous_const).vadd continuous_snd).continuousOn
  convert! AddTorsor.connectedSpace s.direction s

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)

Tactic:
have integrand_eq : ∀ ω,
      ENNReal.ofReal (∫ t in 0..f ω, g t) = ∫⁻ t in Ioc 0 (f ω), ENNReal.ofReal (g t) := by
    intro ω
    have g_ae_nn : 0 ≤ᵐ[volume.restrict (Ioc 0 (f ω))] g := by
      filter_upwards [self_mem_ae_restrict (measurableSet_Ioc : MeasurableSet (Ioc 0 (f ω)))]
        with x hx using g_nn x hx.1
    rw [← ofReal_integral_eq_lintegral_ofReal (g_intble' (f ω) (f_nn ω)).1 g_ae_nn]
    congr
    exact intervalIntegral.integral_of_le (f_nn ω)

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
Module: Mathlib.Analysis.SpecialFunctions.JapaneseBracket

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
⊢ 1 + ‖x‖ ≤ √2 * √(1 + ‖x‖ ^ 2)

Tactic:
rw [← sqrt_mul zero_le_two]

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
⊢ 1 + ‖x‖ ≤ √(2 * (1 + ‖x‖ ^ 2))
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: 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
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ : ∀ (N : ℕ), ∃ k C, ∃ (_ : 0 ≤ C), ∀ n ≤ N, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n g t x‖ ≤ C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
⊢ HasTemperateGrowth (g ∘ f)

Tactic:
refine ⟨hg₁.comp_contDiff hf.1 (ht ⟨·, rfl⟩), fun n ↦ ?_⟩

Goal state after:
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
t : Set E
ht : Set.range f ⊆ t
ht' : UniqueDiffOn ℝ t
hg₁ : ContDiffOn ℝ ∞ g t
hg₂ : ∀ (N : ℕ), ∃ k C, ∃ (_ : 0 ≤ C), ∀ n ≤ N, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n g t x‖ ≤ C * (1 + ‖x‖) ^ k
hf : HasTemperateGrowth f
n : ℕ
⊢ ∃ k C, ∀ (x : D), ‖iteratedFDeriv ℝ n (g ∘ f) x‖ ≤ C * (1 + ‖x‖) ^ k
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
f_nonneg : ∀ (ω : α), 0 ≤ f ω
H1 : ¬g =ᵐ[volume.restrict (Ioi 0)] 0
H2 : ∀ s > 0, 0 < ∫ (t : ℝ) in 0..s, g t → μ {a | s < f a} ≠ ∞
M_bdd : BddAbove {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M : ℝ := sSup {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
zero_mem : 0 ∈ {s | g =ᵐ[volume.restrict (Ioc 0 s)] 0}
M_nonneg : 0 ≤ M
hgM : g =ᵐ[volume.restrict (Ioc 0 M)] 0
ν : Measure α := μ.restrict {a | M < f a}
this : SigmaFinite ν
meas : MeasurableSet {a | M < f a}
I : ∫⁻ (ω : α) in {a | M < f a}ᶜ, ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = 0
⊢ ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂ν

Tactic:
rw [← lintegral_add_compl _ meas, I, add_zero]

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 : ℕ∞
V : Type u_6
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module ℝ V
t : TopologicalSpace V
inst✝⁶ : IsTopologicalAddGroup V
inst✝⁵ : ContinuousSMul ℝ V
inst✝⁴ : LocallyConvexSpace ℝ V
inst✝³ : Algebra ℝ 𝕜
inst✝² : IsScalarTower ℝ 𝕜 F
inst✝¹ : Module 𝕜 V
inst✝ : IsScalarTower ℝ 𝕜 V
f : 𝓓^{n}(Ω, F) →ₗ[𝕜] V
this✝¹ : IsTopologicalAddGroup 𝓓^{n}(Ω, F)
this✝ : ContinuousSMul ℝ 𝓓^{n}(Ω, F)
this : LocallyConvexSpace ℝ 𝓓^{n}(Ω, F)
⊢ ⨆ K, ⨆ (K_sub_Ω : ↑K ⊆ ↑Ω), coinduced (ofSupportedIn K_sub_Ω) ContDiffMapSupportedIn.topologicalSpace ≤
      induced (⇑(↑ℝ f)) t ↔
    ∀ (K : Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω), Continuous[_, t] (⇑(↑ℝ f) ∘ ofSupportedIn K_sub_Ω)

Tactic:
iSup₂_le_iff,

Goal state after:
𝕜 : 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 : ℕ∞
V : Type u_6
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module ℝ V
t : TopologicalSpace V
inst✝⁶ : IsTopologicalAddGroup V
inst✝⁵ : ContinuousSMul ℝ V
inst✝⁴ : LocallyConvexSpace ℝ V
inst✝³ : Algebra ℝ 𝕜
inst✝² : IsScalarTower ℝ 𝕜 F
inst✝¹ : Module 𝕜 V
inst✝ : IsScalarTower ℝ 𝕜 V
f : 𝓓^{n}(Ω, F) →ₗ[𝕜] V
this✝¹ : IsTopologicalAddGroup 𝓓^{n}(Ω, F)
this✝ : ContinuousSMul ℝ 𝓓^{n}(Ω, F)
this : LocallyConvexSpace ℝ 𝓓^{n}(Ω, F)
⊢ (∀ (i : Compacts E) (j : ↑i ⊆ ↑Ω),
      coinduced (ofSupportedIn j) ContDiffMapSupportedIn.topologicalSpace ≤ induced (⇑(↑ℝ f)) t) ↔
    ∀ (K : Compacts E) (K_sub_Ω : ↑K ⊆ ↑Ω), Continuous[_, t] (⇑(↑ℝ f) ∘ ofSupportedIn K_sub_Ω)
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case h
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : E → F
hf : ContDiff ℝ ∞ f ∧ ∀ (n : ℕ), ∃ k, iteratedFDeriv ℝ n f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
hg : ContDiff ℝ ∞ g ∧ ∀ (n : ℕ), ∃ k, iteratedFDeriv ℝ n g =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
n k₁ : ℕ
h₁ : iteratedFDeriv ℝ n f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k₁
k₂ : ℕ
h₂ : iteratedFDeriv ℝ n g =O[⊤] fun x ↦ (1 + ‖x‖) ^ k₂
⊢ (iteratedFDeriv ℝ n f + iteratedFDeriv ℝ n g) =O[⊤] fun x ↦ (1 + ‖x‖) ^ max k₁ k₂

Tactic:
have : 1 ≤ᶠ[⊤] fun (x : E) ↦ 1 + ‖x‖ := by
    filter_upwards with _ using (le_add_iff_nonneg_right _).mpr (by positivity)

Goal state after:
case h
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f g : E → F
hf : ContDiff ℝ ∞ f ∧ ∀ (n : ℕ), ∃ k, iteratedFDeriv ℝ n f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
hg : ContDiff ℝ ∞ g ∧ ∀ (n : ℕ), ∃ k, iteratedFDeriv ℝ n g =O[⊤] fun x ↦ (1 + ‖x‖) ^ k
n k₁ : ℕ
h₁ : iteratedFDeriv ℝ n f =O[⊤] fun x ↦ (1 + ‖x‖) ^ k₁
k₂ : ℕ
h₂ : iteratedFDeriv ℝ n g =O[⊤] fun x ↦ (1 + ‖x‖) ^ k₂
this : 1 ≤ᶠ[⊤] fun x ↦ 1 + ‖x‖
⊢ (iteratedFDeriv ℝ n f + iteratedFDeriv ℝ n g) =O[⊤] fun x ↦ (1 + ‖x‖) ^ max k₁ k₂
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case zero
R : Type u_3
E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedRing R
inst✝ : NormedAlgebra ℝ R
f : E → R
hf : HasTemperateGrowth f
⊢ HasTemperateGrowth (f ^ 0)

Tactic:
| zero =>

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

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : IsTopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
U : Set M₂
hU : U ∈ 𝓝 0
K : Set M₂
hK : IsCompact K
hKf : ⇑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : r > 0
hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
this : σ₁₂ c⁻¹ • K ⊆ U
⊢ σ₁₂ c⁻¹ • K ∈ map (⇑f) (𝓝 0)

Tactic:
have : IsUnit c⁻¹ := hcnz.isUnit.inv

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : IsTopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
U : Set M₂
hU : U ∈ 𝓝 0
K : Set M₂
hK : IsCompact K
hKf : ⇑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : r > 0
hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
this✝ : σ₁₂ c⁻¹ • K ⊆ U
this : IsUnit c⁻¹
⊢ σ₁₂ c⁻¹ • K ∈ map (⇑f) (𝓝 0)
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case h
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : μ.HasTemperateGrowth
f : E → F
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : E), ‖f x‖ ≤ C₁
h'f : ∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
h''f : AEStronglyMeasurable f μ
⊢ ∀ᵐ (a : E) ∂μ, ‖‖a‖ ^ k * ‖f a‖‖ ≤ 2 ^ μ.integrablePower * (C₁ + C₂) * (1 + ‖a‖) ^ (-↑μ.integrablePower)

Tactic:
filter_upwards with v
    simp only [norm_mul, norm_pow, norm_norm]
    apply pow_mul_le_of_le_of_pow_mul_le (norm_nonneg _) (norm_nonneg _) (hf v) (h'f v)

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✝¹ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : Nontrivial E
hT : T.IsSymmetric
this : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact (sphere 0 ‖x‖)
H₂ : (sphere 0 ‖x‖).Nonempty
x₀ : E
hx₀' : x₀ ∈ sphere 0 ‖x‖
hTx₀ : IsMaxOn (↑T').reApplyInnerSelf (sphere 0 ‖x‖) x₀
hx₀ : ‖x₀‖ = ‖x‖
⊢ IsMaxOn (↑T').reApplyInnerSelf (sphere 0 ‖x₀‖) x₀

Tactic:
simpa only [← hx₀] using hTx₀

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✝¹ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : Nontrivial E
hT : T.IsSymmetric
this : ProperSpace E
T' : ↥(selfAdjoint (E →L[𝕜] E)) := hT.toSelfAdjoint
x : E
hx : x ≠ 0
H₁ : IsCompact (sphere 0 ‖x‖)
H₂ : (sphere 0 ‖x‖).Nonempty
x₀ : E
hx₀' : x₀ ∈ sphere 0 ‖x‖
hTx₀ : IsMinOn (↑T').reApplyInnerSelf (sphere 0 ‖x‖) x₀
hx₀ : ‖x₀‖ = ‖x‖
⊢ IsMinOn (↑T').reApplyInnerSelf (sphere 0 ‖x₀‖) x₀

Tactic:
simpa only [← hx₀] using hTx₀

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

Goal state before:
pp: case mp
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : σ = sort f
⊢ StrictMono ⇑((graphEquiv₂ f).trans ((graphEquiv₁ f).symm.trans (graphEquiv₁ f)))

Tactic:
Equiv.symm_trans_self

Goal state after:
case mp
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : σ = sort f
⊢ StrictMono ⇑((graphEquiv₂ f).trans (Equiv.refl ↥(graph f)))
Module: Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative

Goal state before:
pp: case zero
𝕜 : 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)
⊢ IsClosed ↑(V 0)

Tactic:
| zero =>

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
r : ℝ
⊢ ((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary) (diagonal fun x ↦ ↑r) = (algebraMap ℝ (Matrix n n 𝕜)) r

Tactic:
← mul_one (algebraMap _ _ _),

Goal state after:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
r : ℝ
⊢ ((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary) (diagonal fun x ↦ ↑r) = (algebraMap ℝ (Matrix n n 𝕜)) r * 1
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
x : 𝕜
hx : HasUnifEigenvalue T x 1
⊢ HasEigenvalue T ↑(RCLike.re x)

Tactic:
RCLike.conj_eq_iff_re.mp (hT.conj_eigenvalue_eq_self hx)

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
x : 𝕜
hx : HasUnifEigenvalue T x 1
⊢ HasEigenvalue T x
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: case e'_2
𝕜 : 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
μ : 𝕜
hμ : HasEigenvalue T μ
i : Fin n
a✝ : i ∈ Finset.univ
x : 𝕜
hx : HasUnifEigenvalue T x 1
⊢ ↑(RCLike.re x) = μ ↔ ⟨x, hx⟩ = ⟨μ, hμ⟩

Tactic:
RCLike.conj_eq_iff_re.mp (hT.conj_eigenvalue_eq_self hx)

Goal state after:
case e'_2
𝕜 : 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
μ : 𝕜
hμ : HasEigenvalue T μ
i : Fin n
a✝ : i ∈ Finset.univ
x : 𝕜
hx : HasUnifEigenvalue T x 1
⊢ x = μ ↔ ⟨x, hx⟩ = ⟨μ, hμ⟩
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
v : E
i : Fin n
w : EuclideanSpace 𝕜 (Fin n)
⊢ ∀ (a : Fin n),
    w.ofLp a • ↑(hT.eigenvalues hn a) • (hT.eigenvectorBasis hn) a =
      (↑(hT.eigenvalues hn a) * w.ofLp a) • (hT.eigenvectorBasis hn) a

Tactic:
intro a

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
v : E
i : Fin n
w : EuclideanSpace 𝕜 (Fin n)
a : Fin n
⊢ w.ofLp a • ↑(hT.eigenvalues hn a) • (hT.eigenvectorBasis hn) a =
    (↑(hT.eigenvalues hn a) * w.ofLp a) • (hT.eigenvectorBasis hn) a
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
⊢ IsUniformInducing ⇑(ContinuousLinearMap.pi (structureMapCLM 𝕜 n))

Tactic:
isUniformInducing_iff_uniformSpace,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
⊢ comap (⇑(ContinuousLinearMap.pi (structureMapCLM 𝕜 n))) (Pi.uniformSpace fun i ↦ E →ᵇ E [×i]→L[ℝ] F) = uniformSpace
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
⊢ WithSeminorms (ContDiffMapSupportedIn.seminorm 𝕜 E F n K)

Tactic:
by
  let p : SeminormFamily 𝕜 𝓓^{n}_{K}(E, F) ((_ : ℕ) × Fin 1) :=
    SeminormFamily.sigma fun i _ ↦
      (normSeminorm 𝕜 (E →ᵇ (E [×i]→L[ℝ] F))).comp (structureMapLM 𝕜 n i)
  have : WithSeminorms p :=
    withSeminorms_iInf fun i ↦ LinearMap.withSeminorms_induced (norm_withSeminorms _ _) _
  exact this.congr_equiv (Equiv.sigmaUnique _ _).symm

Goal state after: