mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sets.VietorisTopology

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
h : ∀ (s : Set (NonemptyCompacts α)), IsClopen s → s = ∅ ∨ s = univ
s : Set α
hs : IsClopen s
⊢ s = ∅ ∨ s = univ

Tactic:
apply h _ ⟨isClosed_subsets_of_isClosed hs.isClosed, isOpen_subsets_of_isOpen hs.isOpen⟩ |>.imp

Goal state after:
case f
α : Type u_1
inst✝ : TopologicalSpace α
h : ∀ (s : Set (NonemptyCompacts α)), IsClopen s → s = ∅ ∨ s = univ
s : Set α
hs : IsClopen s
⊢ {K | ↑K ⊆ s} = ∅ → s = ∅

case g
α : Type u_1
inst✝ : TopologicalSpace α
h : ∀ (s : Set (NonemptyCompacts α)), IsClopen s → s = ∅ ∨ s = univ
s : Set α
hs : IsClopen s
⊢ {K | ↑K ⊆ s} = univ → s = univ
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∈ c.C → approx n c x = 0
c : CU P
hx : x ∈ c.C
⊢ approx (n + 1) c x = 0

Tactic:
simp only [approx]
    rw [ihn, ihn, midpoint_self]
    exacts [c.subset_right_C hx, hx]

Goal state after:
Module: Mathlib.Topology.UrysohnsLemma

Goal state before:
pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Set X → Prop
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU P), ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ n
c : CU P
hxl : x ∉ c.left.U
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (c.lim x_1) (c.lim x) ≤ (3 / 4) ^ (n + 1)

Tactic:
· replace hxl : x ∈ c.left.right.Cᶜ :=
        compl_subset_compl.2 c.left.right.subset hxl
      filter_upwards [IsOpen.mem_nhds (isOpen_compl_iff.2 c.left.right.closed_C) hxl,
        ihn c.left.right, ihn c.right] with y hyl hydl hydr
      replace hxl : x ∉ c.left.left.U :=
        compl_subset_compl.2 c.left.left_U_subset_right_C hxl
      replace hyl : y ∉ c.left.left.U :=
        compl_subset_compl.2 c.left.left_U_subset_right_C hyl
      simp only [pow_succ, c.lim_eq_midpoint, c.left.lim_eq_midpoint,
        c.left.left.lim_of_notMem_U _ hxl, c.left.left.lim_of_notMem_U _ hyl]
      grw [dist_midpoint_midpoint_le, dist_midpoint_midpoint_le, dist_self, zero_add]
      set r := (3 / 4 : ℝ) ^ n
      calc _ ≤ (r / 2 + r) / 2 := by gcongr
        _ = _ := by ring

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.GelfandDuality

Goal state before:
pp: case insert
A : Type u_1
inst✝ : NonUnitalCommCStarAlgebra A
ι : Type u_2
f : ι → A
h0 : Pairwise ((fun x1 x2 ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : ‖∑ i ∈ s, f i‖₊ = s.sup fun x ↦ ‖f x‖₊
⊢ ‖∑ i ∈ insert j s, f i‖₊ = (insert j s).sup fun x ↦ ‖f x‖₊

Tactic:
suffices f j * ∑ i ∈ s, f i = 0 by simp_all [nnnorm_add_eq_max this]
    simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h0 (by grind)

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_2
S : Type u_3
A : ι → Type u_4
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : Nontrivial R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : MetricSpace R
inst✝¹⁴ : IsTopologicalSemiring R
inst✝¹³ : ContinuousStar R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : (i : ι) → NonUnitalRing (A i)
inst✝⁹ : (i : ι) → Module S (A i)
inst✝⁸ : (i : ι) → Module R (A i)
inst✝⁷ : ∀ (i : ι), IsScalarTower R S (A i)
inst✝⁶ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝⁵ : ∀ (i : ι), IsScalarTower R (A i) (A i)
inst✝⁴ : (i : ι) → StarRing (A i)
inst✝³ : (i : ι) → TopologicalSpace (A i)
p : ((i : ι) → A i) → Prop
q : (i : ι) → A i → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R ((i : ι) → A i) p
inst✝¹ : ∀ (i : ι), NonUnitalContinuousFunctionalCalculus R (A i) (q i)
inst✝ : ∀ (i : ι), ContinuousMapZero.UniqueHom R (A i)
f : R → R
a : (i : ι) → A i
hf : ContinuousOn f (⋃ i, quasispectrum R (a i))
ha : p a
ha' : ∀ (i : ι), q i (a i)
hf₀ : ¬f 0 = 0
⊢ cfcₙ f a = fun i ↦ cfcₙ f (a i)

Tactic:
· simp only [cfcₙ_apply_of_not_map_zero _ hf₀, Pi.zero_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace γ
𝔖 : Set (Set α)
inst✝ : PseudoEMetricSpace β
f : γ → α →ᵤ[𝔖] β
K : Set α → ℝ≥0
h : ∀ s ∈ 𝔖, ∀ c ∈ s, LipschitzWith (K s) fun x ↦ (toFun 𝔖) (f x) c
s : Set α
hs : s ∈ 𝔖
⊢ LipschitzWith (K s) (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(toFun 𝔖) ∘ f)

Tactic:
rw [UniformFun.lipschitzWith_iff]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PseudoEMetricSpace γ
𝔖 : Set (Set α)
inst✝ : PseudoEMetricSpace β
f : γ → α →ᵤ[𝔖] β
K : Set α → ℝ≥0
h : ∀ s ∈ 𝔖, ∀ c ∈ s, LipschitzWith (K s) fun x ↦ (toFun 𝔖) (f x) c
s : Set α
hs : s ∈ 𝔖
⊢ ∀ (c : ↑s), LipschitzWith (K s) fun x ↦ UniformFun.toFun ((⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(toFun 𝔖) ∘ f) x) c
Module: Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart

Goal state before:
pp: case refine_2
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
r : ℝ
hr : 0 < r
x : A
hx : x ∈ {a | 0 ≤ a}
hx_pos : 0 < ‖x‖
this : (↑r * ↑‖x‖⁻¹)⁻¹ • (↑r * ↑‖x‖⁻¹) • x = x
⊢ (↑r * ↑‖x‖⁻¹) • x ∈ Metric.closedBall 0 r

Tactic:
simp [mul_smul, norm_smul, abs_of_pos hr, inv_mul_cancel₀ hx_pos.ne']

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarRing A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ ℝ≥0 a)
hg0 : g 0 = 0
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
⊢ cfcₙ (fun x ↦ f x - g x) a = cfcₙ f a - cfcₙ g a

Tactic:
have : (σₙ ℝ a).EqOn (fun x ↦ ((f x.toNNReal - g x.toNNReal : ℝ≥0) : ℝ))
      (fun x ↦ f x.toNNReal - g x.toNNReal) :=
    fun x hx ↦ NNReal.coe_sub <| hfg _ <| ha'.apply_mem hx

Goal state after:
A : Type u_1
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarRing A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ ℝ≥0 a)
hg0 : g 0 = 0
ha' : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
this : Set.EqOn (fun x ↦ ↑(f x.toNNReal - g x.toNNReal)) (fun x ↦ ↑(f x.toNNReal) - ↑(g x.toNNReal)) (σₙ ℝ a)
⊢ cfcₙ (fun x ↦ f x - g x) a = cfcₙ f a - cfcₙ g a
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
ha : 0 ≤ a
⊢ sqrt a ^ ↑x = a ^ (↑x / 2)

Tactic:
by_cases hx : x = 0
  case pos =>
    have ha' : 0 ≤ sqrt a := sqrt_nonneg _
    simp [hx, rpow_zero _ ha', rpow_zero _ ha]
  case neg =>
    have h₁ : 0 ≤ (x : ℝ) := NNReal.zero_le_coe
    rw [sqrt_eq_rpow, rpow_rpow_of_exponent_nonneg _ _ _ (by simp) h₁, one_div_mul_eq_div]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: ⊢ (fun x ↦ x * (1 + x)⁻¹) = fun x ↦ 1 - (1 + x)⁻¹

Tactic:
ext x : 1

Goal state after:
x : ℝ≥0
⊢ x * (1 + x)⁻¹ = 1 - (1 + x)⁻¹
Module: Mathlib.Topology.UniformSpace.Matrix

Goal state before:
pp: m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
β : Type u_4
inst✝ : UniformSpace β
f : β → Matrix m n 𝕜
⊢ (∀ (i : m) (i_1 : n), Filter.Tendsto ((fun a ↦ (a.1 i i_1, a.2 i i_1)) ∘ fun x ↦ (f x.1, f x.2)) (𝓤 β) (𝓤 𝕜)) ↔
    ∀ (i : m) (j : n), Filter.Tendsto (fun x ↦ (f x.1 i j, f x.2 i j)) (𝓤 β) (𝓤 𝕜)

Tactic:
apply Iff.intro

Goal state after:
case mp
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
β : Type u_4
inst✝ : UniformSpace β
f : β → Matrix m n 𝕜
⊢ (∀ (i : m) (i_1 : n), Filter.Tendsto ((fun a ↦ (a.1 i i_1, a.2 i i_1)) ∘ fun x ↦ (f x.1, f x.2)) (𝓤 β) (𝓤 𝕜)) →
    ∀ (i : m) (j : n), Filter.Tendsto (fun x ↦ (f x.1 i j, f x.2 i j)) (𝓤 β) (𝓤 𝕜)

case mpr
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝¹ : UniformSpace 𝕜
β : Type u_4
inst✝ : UniformSpace β
f : β → Matrix m n 𝕜
⊢ (∀ (i : m) (j : n), Filter.Tendsto (fun x ↦ (f x.1 i j, f x.2 i j)) (𝓤 β) (𝓤 𝕜)) →
    ∀ (i : m) (i_1 : n), Filter.Tendsto ((fun a ↦ (a.1 i i_1, a.2 i i_1)) ∘ fun x ↦ (f x.1, f x.2)) (𝓤 β) (𝓤 𝕜)
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ‖toLp 2 fun i ↦ toLp 2 fun j ↦ A i j‖₊ = (∑ i, ∑ j, ‖A i j‖₊ ^ 2) ^ (1 / 2)

Tactic:
simp_rw [PiLp.nnnorm_eq_of_L2, NNReal.sq_sqrt, NNReal.sqrt_eq_rpow, NNReal.rpow_two]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute

Goal state before:
pp: case mul
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra 𝕜 A
inst✝³ : TopologicalSpace A
inst✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f g : C(↑(spectrum 𝕜 a), 𝕜)
hf : Commute ((cfcHom ha) f) b
hg : Commute ((cfcHom ha) g) b
⊢ Commute ((cfcHom ha) (f * g)) b

Tactic:
rw [map_mul]; exact mul_left hf hg

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute

Goal state before:
pp: A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : TopologicalSpace A
inst✝² : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
hb : Commute a b
f : ℝ → ℝ
hf : ContinuousOn f (spectrum ℝ a)
ha : IsSelfAdjoint a
⊢ Commute (cfc f a) b

Tactic:
exact hb.cfc (ha.star_eq.symm ▸ hb) _

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute

Goal state before:
pp: case mul
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f g : C(↑(quasispectrum 𝕜 a), 𝕜)₀
hf : Commute ((cfcₙHom ha) f) b
hg : Commute ((cfcₙHom ha) g) b
⊢ Commute ((cfcₙHom ha) (f * g)) b

Tactic:
rw [map_mul]; exact mul_left hf hg

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : MeasurableSpace X
μ : Measure X
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : CompleteSpace A
inst✝ : NormedSpace ℝ A
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 a)
hf₂ : Integrable (fun x ↦ mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
key₁ : ∀ (z : ↑(spectrum 𝕜 a)), ∫ (x : X), f x ↑z ∂μ = (∫ (x : X), mkD ((spectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z
⊢ cfc (fun z ↦ ∫ (x : X), f x z ∂μ) a = ∫ (x : X), cfc (f x) a ∂μ

Tactic:
have key₂ (z : spectrum 𝕜 a) :
      ∫ x, f x z ∂μ = mkD ((spectrum 𝕜 a).domRestrict (fun z ↦ ∫ x, f x z ∂μ)) 0 z := by
    rw [mkD_apply_of_continuousOn]
    rw [continuousOn_iff_continuous_domRestrict]
    refine continuous_congr key₁ |>.mpr ?_
    exact map_continuous (∫ x, mkD ((spectrum 𝕜 a).domRestrict (f x)) 0 ∂μ)

Goal state after:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : MeasurableSpace X
μ : Measure X
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : CompleteSpace A
inst✝ : NormedSpace ℝ A
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 a)
hf₂ : Integrable (fun x ↦ mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
key₁ : ∀ (z : ↑(spectrum 𝕜 a)), ∫ (x : X), f x ↑z ∂μ = (∫ (x : X), mkD ((spectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z
key₂ :
  ∀ (z : ↑(spectrum 𝕜 a)), ∫ (x : X), f x ↑z ∂μ = (mkD ((spectrum 𝕜 a).domRestrict fun z ↦ ∫ (x : X), f x z ∂μ) 0) z
⊢ cfc (fun z ↦ ∫ (x : X), f x z ∂μ) a = ∫ (x : X), cfc (f x) a ∂μ
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart

Goal state before:
pp: A : Type u_1
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : Algebra ℂ A
inst✝¹ : StarModule ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
hp : IsStarNormal a
⊢ cfc (fun x ↦ ↑x.im) a = ↑(ℑ a)

Tactic:
suffices cfc (fun z : ℂ ↦ re z + I * im z) a = ℜ a + I • ℑ a by
    rw [cfc_add .., cfc_const_mul .., cfc_re_id a] at this
    simpa
  simp [mul_comm I, re_add_im, cfc_id' .., realPart_add_I_smul_imaginaryPart]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.NullSubmodule

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
⊢ IsClosed ↑(nullSubgroup M)

Tactic:
apply isClosed_singleton.preimage continuous_norm'

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Semiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A B C : Set E
hAB : IsExtreme 𝕜 A B
hBC : IsExtreme 𝕜 B C
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
x : E
hxC : x ∈ C
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ ∈ C

Tactic:
exact hBC.left_mem_of_mem_openSegment
    (hAB.left_mem_of_mem_openSegment hx₁A hx₂A (hBC.subset hxC) hx)
    (hAB.right_mem_of_mem_openSegment hx₁A hx₂A (hBC.subset hxC) hx) hxC hx

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
e✝ : Pretrivialization F proj
x : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
e : Pretrivialization F fun z ↦ proj ↑z
inst✝ : Nonempty (Z → F)
⊢ Subtype.val '' e.source = proj ⁻¹' e.baseSet

Tactic:
ext z; simpa [e.source_eq] using
    (e.proj_symm_apply' · ▸ (e.invFun (proj z, Classical.arbitrary (Z → F) z)).2)

Goal state after:
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ IsLocallyInjective f ↔ IsOpen[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)

Tactic:
by
  simp_rw [isLocallyInjective_iff_nhds, isOpen_iff_mem_nhds,
    Subtype.forall, Prod.forall, nhds_induced, nhds_prod_eq, Filter.mem_comap]
  refine ⟨?_, fun h x ↦ ?_⟩
  · rintro h x x' hx (rfl : x = x')
    obtain ⟨U, hn, hi⟩ := h x
    exact ⟨_, Filter.prod_mem_prod hn hn, fun {p} hp ↦ hi hp.1 hp.2 p.2⟩
  · obtain ⟨t, ht, t_sub⟩ := h x x rfl rfl
    obtain ⟨t₁, h₁, t₂, h₂, prod_sub⟩ := Filter.mem_prod_iff.mp ht
    exact ⟨t₁ ∩ t₂, Filter.inter_mem h₁ h₂,
      fun x₁ h₁ x₂ h₂ he ↦ @t_sub ⟨(x₁, x₂), he⟩ (prod_sub ⟨h₁.1, h₂.2⟩)⟩

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: case e'_3
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CStarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖f b‖₊ ^ 2 ≤ C * ‖f b‖₊ * ‖b‖₊
h1 : ∀ (b : A), C * ‖f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2
this : ‖f‖₊ / sqrt ‖f‖₊ ≤ sqrt C
⊢ ‖f‖₊ = (‖f‖₊ / sqrt ‖f‖₊) ^ 2

Tactic:
simp only [NNReal.rpow_two, div_pow, sq_sqrt]
      simp only [sq, mul_self_div_self]

Goal state after:
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hgf✝ : IsLocalHomeomorphOn (g ∘ ↑f) s
hf : IsLocalHomeomorphOn (↑f) s
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ ↑f = ↑gf
y : Y
hy : y ∈ (f.symm.trans gf).source
⊢ g y = g (↑f (↑f.symm y))

Tactic:
f.right_inv hy.1

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
s : Set X
x : X
hx : x ∈ s
f : OpenPartialHomeomorph X Y
hxf : x ∈ f.source
hgf✝ : IsLocalHomeomorphOn (g ∘ ↑f) s
hf : IsLocalHomeomorphOn (↑f) s
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : g ∘ ↑f = ↑gf
y : Y
hy : y ∈ (f.symm.trans gf).source
⊢ g y = g y
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case h
x✝ : ℝ
⊢ (-↑x✝).toCircle = (↑x✝).toCircle⁻¹

Tactic:
simp_rw [← coe_neg, toCircle_coe, Circle.exp_neg]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Maps

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : CStarRing A
inst✝² : Ring R
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
u v : ↥(unitary A)
⊢ (mulRight R u).trans (mulRight R v) = mulRight R (u * v)

Tactic:
ext; simp [mul_assoc]

Goal state after:
Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone

Goal state before:
pp: f : ℝ → ℝ
s : Set ℝ
c : ℝ
hc : 0 ≤ c
p : ℝ → FormalMultilinearSeries ℝ ℝ ℝ
hp : HasFTaylorSeriesUpToOn ∞ f p s
hp_nn : ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → 0 ≤ (p x n) fun x ↦ 1
T : ℝ →L[ℝ] ℝ := c • ContinuousLinearMap.id ℝ ℝ
hT : T = c • ContinuousLinearMap.id ℝ ℝ
⊢ AbsolutelyMonotoneOn (c • f) s

Tactic:
have hcomp : (T ∘ f) = c • f := by ext x; simp [hT, smul_eq_mul]

Goal state after:
f : ℝ → ℝ
s : Set ℝ
c : ℝ
hc : 0 ≤ c
p : ℝ → FormalMultilinearSeries ℝ ℝ ℝ
hp : HasFTaylorSeriesUpToOn ∞ f p s
hp_nn : ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → 0 ≤ (p x n) fun x ↦ 1
T : ℝ →L[ℝ] ℝ := c • ContinuousLinearMap.id ℝ ℝ
hT : T = c • ContinuousLinearMap.id ℝ ℝ
hcomp : ⇑T ∘ f = c • f
⊢ AbsolutelyMonotoneOn (c • f) s
Module: Mathlib.MeasureTheory.Group.Integral

Goal state before:
pp: G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Group G
inst✝¹ : MeasurableInv G
f : G → E
μ : Measure G
inst✝ : μ.IsInvInvariant
h : MeasurableEmbedding fun x ↦ x⁻¹
⊢ ∫ (x : G), f x⁻¹ ∂μ = ∫ (x : G), f x ∂μ

Tactic:
rw [← h.integral_map, map_inv_eq_self]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C
⊢ Memℓp f p

Tactic:
apply memℓp_gen
  use ⨆ s : Finset α, ∑ i ∈ s, ‖f i‖ ^ p.toReal
  apply hasSum_of_isLUB_of_nonneg
  · intro b
    positivity
  apply isLUB_ciSup
  use C
  rintro - ⟨s, rfl⟩
  exact hf s

Goal state after:
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: case succ
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
k : ℕ
IH : ↑k ≤ N → (iteratedFDeriv 𝕜 k fun y ↦ ∑' (n : α), f n y) = fun x ↦ ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
hk : ↑(k + 1) ≤ N
h'k : ↑k < N
⊢ (iteratedFDeriv 𝕜 (k + 1) fun y ↦ ∑' (n : α), f n y) = fun x ↦ ∑' (n : α), iteratedFDeriv 𝕜 (k + 1) (f n) x

Tactic:
have A : Summable fun n => iteratedFDeriv 𝕜 k (f n) 0 :=
      .of_norm_bounded (hv k h'k.le) fun n ↦ h'f k n 0 h'k.le

Goal state after:
case succ
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
k : ℕ
IH : ↑k ≤ N → (iteratedFDeriv 𝕜 k fun y ↦ ∑' (n : α), f n y) = fun x ↦ ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
hk : ↑(k + 1) ≤ N
h'k : ↑k < N
A : Summable fun n ↦ iteratedFDeriv 𝕜 k (f n) 0
⊢ (iteratedFDeriv 𝕜 (k + 1) fun y ↦ ∑' (n : α), f n y) = fun x ↦ ∑' (n : α), iteratedFDeriv 𝕜 (k + 1) (f n) x
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case e'_4
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 E'
inst✝² : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝¹ : AddGroup G
inst✝ : TopologicalSpace G
hcf : HasCompactSupport f
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
x t : G
s : Set G
hx : x ∈ s
⊢ (-tsupport f + s).indicator (fun t ↦ (‖L‖ * ⨆ i, ‖f i‖) * ‖g t‖) t =
    (-tsupport f + s).indicator (fun t ↦ ‖L.flip‖ * ‖g t‖ * ⨆ i, ‖f i‖) t

Tactic:
simp_rw [L.opNorm_flip, mul_right_comm]

Goal state after:
Module: Mathlib.Analysis.Calculus.ParametricIntegral

Goal state before:
pp: α : Type u_1
inst✝⁶ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (F' a) x₀
δ : ℝ
δ_pos : δ > 0
hδ_meas : ∀ x ∈ ball x₀ δ, AEStronglyMeasurable (F x) μ
hδε : ∀ x ∈ ball x₀ δ, x ∈ s
h_lip : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ δ, ‖F x a - F x₀ a‖ ≤ |bound a| * ‖x - x₀‖
⊢ Integrable F' μ ∧ HasFDerivAt (fun x ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

Tactic:
replace bound_integrable := bound_integrable.norm

Goal state after:
α : Type u_1
inst✝⁶ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (F' a) x₀
δ : ℝ
δ_pos : δ > 0
hδ_meas : ∀ x ∈ ball x₀ δ, AEStronglyMeasurable (F x) μ
hδε : ∀ x ∈ ball x₀ δ, x ∈ s
h_lip : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ δ, ‖F x a - F x₀ a‖ ≤ |bound a| * ‖x - x₀‖
bound_integrable : Integrable (fun a ↦ ‖bound a‖) μ
⊢ Integrable F' μ ∧ HasFDerivAt (fun x ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀