mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral

Goal state before:
pp: case refine_1
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : RCLike 𝕜
inst✝¹¹ : MeasurableSpace X
μ : Measure X
inst✝¹⁰ : NonUnitalNormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : NormedSpace 𝕜 A
inst✝⁷ : IsScalarTower 𝕜 A A
inst✝⁶ : SMulCommClass 𝕜 A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝⁴ : CompleteSpace A
inst✝³ : NormedSpace ℝ A
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)
hf : ContinuousOn (uncurry f) (univ ×ˢ quasispectrum 𝕜 a)
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound μ
ha : p a
this : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)
⊢ AEStronglyMeasurable (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ

pp: case refine_2
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : RCLike 𝕜
inst✝¹¹ : MeasurableSpace X
μ : Measure X
inst✝¹⁰ : NonUnitalNormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : NormedSpace 𝕜 A
inst✝⁷ : IsScalarTower 𝕜 A A
inst✝⁶ : SMulCommClass 𝕜 A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝⁴ : CompleteSpace A
inst✝³ : NormedSpace ℝ A
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)
hf : ContinuousOn (uncurry f) (univ ×ˢ quasispectrum 𝕜 a)
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound μ
ha : p a
this : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)
⊢ HasFiniteIntegral (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ

Tactic:
· exact aeStronglyMeasurable_mkD_restrict_of_uncurry _ _ hf f_zero

Goal state after:
case refine_2
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : RCLike 𝕜
inst✝¹¹ : MeasurableSpace X
μ : Measure X
inst✝¹⁰ : NonUnitalNormedRing A
inst✝⁹ : StarRing A
inst✝⁸ : NormedSpace 𝕜 A
inst✝⁷ : IsScalarTower 𝕜 A A
inst✝⁶ : SMulCommClass 𝕜 A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝⁴ : CompleteSpace A
inst✝³ : NormedSpace ℝ A
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
f : X → 𝕜 → 𝕜
bound : X → ℝ
a : A
inst✝ : SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)
hf : ContinuousOn (uncurry f) (univ ×ˢ quasispectrum 𝕜 a)
f_zero : ∀ᵐ (x : X) ∂μ, f x 0 = 0
bound_ge : ∀ᵐ (x : X) ∂μ, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x
bound_int : HasFiniteIntegral bound μ
ha : p a
this : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)
⊢ HasFiniteIntegral (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: case refine_3
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x : E
y : F
hx : (x, y) ∈ s ×ˢ t
h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → (x, y) ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y)
x₁ : F
hx₁ : x₁ ∈ t
x₂ : F
hx₂ : x₂ ∈ t
hx_snd : (x, y).2 ∈ openSegment 𝕜 x₁ x₂
⊢ (x, y) ∈ openSegment 𝕜 ((x, y).1, x₁) ((x, y).1, x₂)

Tactic:
← Prod.image_mk_openSegment_right

Goal state after:
case refine_3
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Semiring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
t : Set F
x : E
y : F
hx : (x, y) ∈ s ×ˢ t
h : ∀ ⦃x₁ : E × F⦄, x₁ ∈ s ×ˢ t → ∀ ⦃x₂ : E × F⦄, x₂ ∈ s ×ˢ t → (x, y) ∈ openSegment 𝕜 x₁ x₂ → x₁ = (x, y)
x₁ : F
hx₁ : x₁ ∈ t
x₂ : F
hx₂ : x₂ ∈ t
hx_snd : (x, y).2 ∈ openSegment 𝕜 x₁ x₂
⊢ (x, y) ∈ (fun y_1 ↦ ((x, y).1, y_1)) '' openSegment 𝕜 x₁ x₂
Module: Mathlib.Analysis.Complex.Circle

Goal state before:
pp: ⊢ probChar ≠ 1

Tactic:
by
  rw [DFunLike.ne_iff]
  use Real.pi
  simpa only [probChar_apply'] using! Circle.exp_pi_ne_one

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen[inst✝] s
s' : Set X
hs' : IsOpen[inst✝] s'
⊢ (ofSet s hs).trans (ofSet s' hs') = ofSet (s ∩ s') ⋯

Tactic:
rw [(ofSet s hs).trans_ofSet hs']

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen[inst✝] s
s' : Set X
hs' : IsOpen[inst✝] s'
⊢ (ofSet s hs).restr (↑(ofSet s hs) ⁻¹' s') = ofSet (s ∩ s') ⋯
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
hyV : ↑e.symm y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
⊢ ↑(V.openPartialHomeomorphSubtypeCoe hV) (↑(V.openPartialHomeomorphSubtypeCoe hV).symm (↑e.symm y)) =
    ↑(V.openPartialHomeomorphSubtypeCoe hV) (i (↑(U.openPartialHomeomorphSubtypeCoe hU).symm (↑e.symm y)))

Tactic:
(V.openPartialHomeomorphSubtypeCoe hV).right_inv hyV

Goal state after:
case refine_2
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
hyV : ↑e.symm y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
⊢ ↑e.symm y = ↑(V.openPartialHomeomorphSubtypeCoe hV) (i (↑(U.openPartialHomeomorphSubtypeCoe hU).symm (↑e.symm y)))
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : Nonempty F
e e' : Pretrivialization F proj
h : e.toPartialEquiv = e'.toPartialEquiv
⊢ e.baseSet = e'.baseSet

Tactic:
simpa only [fst_image_prod, univ_nonempty, target_eq]
    using congr_arg (Prod.fst '' PartialEquiv.target ·) h

Goal state after:
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: X : Type u_1
E : Type u_2
A : Type u_3
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace A
p : E → X
s : Set A
g₁ g₂ : A → E
sep : IsSeparatedMap p
inj : IsLocallyInjective p
hs : IsPreconnected s
h₁ : ContinuousOn g₁ s
h₂ : ContinuousOn g₂ s
he : s.domRestrict (p ∘ g₁) = s.domRestrict (p ∘ g₂)
a : A
has : a ∈ s
ha : g₁ a = g₂ a
⊢ s.domRestrict g₁ = s.domRestrict g₂

Tactic:
continuousOn_iff_continuous_domRestrict

Goal state after:
X : Type u_1
E : Type u_2
A : Type u_3
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace A
p : E → X
s : Set A
g₁ g₂ : A → E
sep : IsSeparatedMap p
inj : IsLocallyInjective p
hs : IsPreconnected s
h₁ : Continuous[instTopologicalSpaceSubtype, inst✝¹] (s.domRestrict g₁)
h₂ : Continuous[instTopologicalSpaceSubtype, inst✝¹] (s.domRestrict g₂)
he : s.domRestrict (p ∘ g₁) = s.domRestrict (p ∘ g₂)
a : A
has : a ∈ s
ha : g₁ a = g₂ a
⊢ s.domRestrict g₁ = s.domRestrict g₂
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: case refine_2
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CStarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : (Metric.closedBall 0 1).Nonempty
key : ∀ (x y : A), ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖a.toProd.2 (star (a.toProd.1 (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' : sqrt r < sSup ((fun x ↦ ‖a.toProd.1 x‖₊) '' Metric.closedBall 0 1)
x : A
hx : x ∈ Metric.closedBall 0 1
hxr : sqrt r < (fun x ↦ ‖a.toProd.1 x‖₊) x
hx' : ‖x‖₊ ≤ 1
⊢ r < sSup ((fun x_1 ↦ ‖a.toProd.2 (star (a.toProd.1 (star (star x)))) * x_1‖₊) '' Metric.closedBall 0 1)

Tactic:
refine lt_csSup_of_lt ?_ ⟨x, hx, rfl⟩ ?_

Goal state after:
case refine_2.refine_1
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CStarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : (Metric.closedBall 0 1).Nonempty
key : ∀ (x y : A), ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖a.toProd.2 (star (a.toProd.1 (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' : sqrt r < sSup ((fun x ↦ ‖a.toProd.1 x‖₊) '' Metric.closedBall 0 1)
x : A
hx : x ∈ Metric.closedBall 0 1
hxr : sqrt r < (fun x ↦ ‖a.toProd.1 x‖₊) x
hx' : ‖x‖₊ ≤ 1
⊢ BddAbove ((fun x_1 ↦ ‖a.toProd.2 (star (a.toProd.1 (star (star x)))) * x_1‖₊) '' Metric.closedBall 0 1)

case refine_2.refine_2
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CStarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : (Metric.closedBall 0 1).Nonempty
key : ∀ (x y : A), ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖a.toProd.2 (star (a.toProd.1 (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊
r : ℝ≥0
hr : r < ‖a‖₊ * ‖a‖₊
hr' : sqrt r < sSup ((fun x ↦ ‖a.toProd.1 x‖₊) '' Metric.closedBall 0 1)
x : A
hx : x ∈ Metric.closedBall 0 1
hxr : sqrt r < (fun x ↦ ‖a.toProd.1 x‖₊) x
hx' : ‖x‖₊ ≤ 1
⊢ r < (fun x_1 ↦ ‖a.toProd.2 (star (a.toProd.1 (star (star x)))) * x_1‖₊) x
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
hf : IsCoveringMap f
t : Set X
⊢ IsCoveringMap (t.restrictPreimage f)

Tactic:
rw [isCoveringMap_iff_isCoveringMapOn_univ] at hf ⊢

Goal state after:
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
hf : IsCoveringMapOn f Set.univ
t : Set X
⊢ IsCoveringMapOn (t.restrictPreimage f) Set.univ
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
hf : IsCoveringMap f
E' : Type u_3
inst✝ : TopologicalSpace E'
g : E' ≃ₜ E
⊢ IsCoveringMap (f ∘ ⇑g)

Tactic:
rw [isCoveringMap_iff_isCoveringMapOn_univ] at hf ⊢

Goal state after:
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
hf : IsCoveringMapOn f Set.univ
E' : Type u_3
inst✝ : TopologicalSpace E'
g : E' ≃ₜ E
⊢ IsCoveringMapOn (f ∘ ⇑g) Set.univ
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
hf : IsCoveringMap f
Y : Type u_3
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
⊢ IsCoveringMap (⇑g ∘ f)

Tactic:
rw [isCoveringMap_iff_isCoveringMapOn_univ] at hf ⊢

Goal state after:
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
hf : IsCoveringMapOn f Set.univ
Y : Type u_3
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
⊢ IsCoveringMapOn (⇑g ∘ f) Set.univ
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
Y : Type u_3
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
h : IsCoveringMap (⇑g ∘ f)
⊢ IsCoveringMap f

Tactic:
by convert! h.homeomorph_comp g.symm; ext; simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case refine_3
x y : Circle
hxy : x ≠ y
⊢ {x, y}ᶜ ∩ (range ⇑(x.path y) ∩ range ⇑(y.path x)) = ∅

Tactic:
(Tactic.tacticSeq
 (Tactic.tacticSeq1Indented
  [(Tactic.rwSeq
    "rw"
    (Tactic.optConfig [])
    (Tactic.rwRuleSeq "[" [(Tactic.rwRule [] (Term.app `range_path_inter_range_path [`hxy]))] "]")
    [])
   []
   (Tactic.exact
    "exact"
    (Term.app
     `compl_inter_self
     [(choice
       («term{_}» "{" [`x "," `y] "}")
       (Term.structInst
        "{"
        []
        (Term.structInstFields
         [(Term.structInstField (Term.structInstLVal `x []) [])
          ","
          (Term.structInstField (Term.structInstLVal `y []) [])])
        (Term.optEllipsis [])
        []
        "}"))]))]))

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: T : ℝ
hT : T ≠ 0
x : AddCircle T
⊢ (homeomorphCircle hT) x = x.toCircle

Tactic:
by
  cases x using QuotientAddGroup.induction_on
  rw [homeomorphCircle, Homeomorph.trans_apply,
    homeomorphAddCircle_apply_mk, homeomorphCircle'_apply_mk, toCircle_apply_mk]
  ring_nf

Goal state after:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
inst✝ : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h : ∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f
⊢ IsEvenlyCovered f x ↑(f ⁻¹' {x})

Tactic:
by
  have : DiscreteTopology (f ⁻¹' {x}) :=
    (IsDiscrete.of_openPartialHomeomorph f subset_rfl h).1
  /- for each preimage e of x, choose a homeomorphism φₑ
    from a neighborhood of e to its image -/
  choose φ hφ using fun e : f ⁻¹' {x} ↦ h e e.2
  -- separately, choose pairwise disjoint neighborhoods Vₑ by Hausdorff-ness
  have ⟨V, hV, disj⟩ := fin.t2_separation
  -- let Vₑ' be the intersection Vₑ ∩ dom(φₑ)
  let V' (e : f ⁻¹' {x}) := V e ∩ (φ e).source
  have hV' e : IsOpen (V' e) := (hV e).2.inter (φ e).open_source
  have : ⋃ e, V' e ∈ nhdsSet (f ⁻¹' {x}) :=
    (isOpen_iUnion hV').mem_nhdsSet.2 fun e he ↦ mem_iUnion_of_mem ⟨e, he⟩ ⟨(hV e).1, (hφ _).1⟩
  -- since f is a closed map, the union of the Vₑ' contains the preimage of a neighborhood U of x
  have ⟨W, hWx, hWV⟩ := isClosedMap_iff_comap_nhds_le.mp hf this
  cases isEmpty_or_nonempty (f ⁻¹' {x})
  · exact .of_preimage_eq_empty _ hWx (by simpa using hWV)
  have ⟨U, hUW, hU, hxU⟩ := mem_nhds_iff.mp hWx
  -- show that the intersection of U with the images of Vₑ' is evenly covered
  let U' := U ∩ ⋂ e : f ⁻¹' {x}, f '' (V' e)
  have : Finite (f ⁻¹' {x}) := fin
  have hU' : IsOpen U' := hU.inter <| isOpen_iInter_of_finite fun e ↦ by
    convert! ← (φ e).isOpen_image_of_subset_source (hV' _) inter_subset_right; exact (hφ e).2
  have hUV e : U' ⊆ f '' V' e := inter_subset_right.trans (iInter_subset ..)
  have : Nonempty E := ⟨Classical.arbitrary (f ⁻¹' {x})⟩
  refine .of_trivialization (t := hU'.trivializationDiscrete _ _
    (fun e s hs ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩) (fun e ↦ ?_)
    (fun e ↦ .mono subset_rfl (hUV e) (surjOn_image f _))
    (pairwise_disjoint_mono disj.subtype fun e ↦ inter_subset_left)
    ((preimage_mono (inter_subset_left.trans hUW)).trans hWV))
    ⟨hxU, Set.mem_iInter.mpr fun e ↦ ⟨e, ⟨(hV e).1, (hφ e).1⟩, e.2⟩⟩
  · convert! ((φ e).isOpen_inter_preimage h).inter (hV e).2 using 1
    simp_rw [(hφ e).2, V']; ac_rfl
  · have : s ⊆ (φ e).target := hs.trans <| (hUV e).trans <| by
      rw [← (φ e).image_source_eq_target, (hφ e).2]; exact image_mono inter_subset_right
    rw [← (φ e).isOpen_symm_image_iff_of_subset_target this,
      (φ e).symm_image_eq_source_inter_preimage this, (hφ e).2, inter_comm]
    convert! h using 1
    refine inter_eq_inter_iff_left.mpr ⟨fun e' h ↦ h.2.2, fun e' h ↦ ⟨?_ , h.2⟩⟩
    have ⟨e'', ⟨_, mem⟩, eq⟩ := mem_iInter.mp (hs h.1).2 e
    rwa [← (φ e).injOn mem h.2 (by rwa [(hφ e).2])]
  · convert! ← (φ e).injOn.mono inter_subset_right; exact (hφ e).2

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : t ∈ Set.Icc 0 1
hu : ‖↑u - 1‖ < 2
⊢ ‖↑(t • argSelfAdjoint u)‖ ≤ 1 * ‖↑(argSelfAdjoint u)‖

Tactic:
val_smul,

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : t ∈ Set.Icc 0 1
hu : ‖↑u - 1‖ < 2
⊢ ‖t • ↑(argSelfAdjoint u)‖ ≤ 1 * ‖↑(argSelfAdjoint u)‖
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
this : re ⟪(adjoint A ∘SL A) x, x⟫_𝕜 ≤ ‖adjoint A ∘SL A‖ * ‖x‖ * ‖x‖
⊢ √(‖adjoint A ∘SL A‖ * (‖x‖ * ‖x‖)) = √‖adjoint A ∘SL A‖ * ‖x‖

Tactic:
Real.sqrt_mul (norm_nonneg _) (‖x‖ * ‖x‖),

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
this : re ⟪(adjoint A ∘SL A) x, x⟫_𝕜 ≤ ‖adjoint A ∘SL A‖ * ‖x‖ * ‖x‖
⊢ √‖adjoint A ∘SL A‖ * √(‖x‖ * ‖x‖) = √‖adjoint A ∘SL A‖ * ‖x‖
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
p : E →L[𝕜] E
⊢ (∃ K, ∃ (x : K.HasOrthogonalProjection), p = K.starProjection) → IsStarProjection p

Tactic:
rintro ⟨_, _, rfl⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
w✝¹ : Submodule 𝕜 E
w✝ : w✝¹.HasOrthogonalProjection
⊢ IsStarProjection w✝¹.starProjection
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
ha : ∀ (x : Fin (n + 1)), (↑fs₁).indicator (centroidWeights k fs₁) x = (↑fs₂).indicator (centroidWeights k fs₂) x
⊢ fs₁ = fs₂

Tactic:
Finset.centroidWeights,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : CharZero k
n : ℕ
s : Simplex k P n
fs₁ fs₂ : Finset (Fin (n + 1))
m₁ m₂ : ℕ
h₁ : #fs₁ = m₁ + 1
h₂ : #fs₂ = m₂ + 1
h :
  (affineCombination k univ s.points) (centroidWeightsIndicator k fs₁) =
    (affineCombination k univ s.points) (centroidWeightsIndicator k fs₂)
ha :
  ∀ (x : Fin (n + 1)),
    (↑fs₁).indicator (Function.const (Fin (n + 1)) (↑(#fs₁))⁻¹) x =
      (↑fs₂).indicator (Function.const (Fin (n + 1)) (↑(#fs₂))⁻¹) x
⊢ fs₁ = fs₂
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
T : E →ₗ[𝕜] E
x : E
⊢ 0 ≤ ‖T x‖ ^ 2

Tactic:
exact sq_nonneg _

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
s : Finset ι
n : ℕ
hc : #s = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
⊢ finrank k ↥(vectorSpan k ↑(Finset.image p s)) ≤ n

Tactic:
vectorSpan_eq_span_vsub_finset_right_ne k hp₁

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
s : Finset ι
n : ℕ
hc : #s = n + 1
p₁ : P
hp₁ : p₁ ∈ Finset.image p s
⊢ finrank k ↥(Submodule.span k ↑(Finset.image (fun x ↦ x -ᵥ p₁) ((Finset.image p s).erase p₁))) ≤ n
Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p ↦ ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y ↦ (lineMap q y) (ε / dist y q)
y : P
⊢ dist ((lineMap q y) (ε / dist y q)) q ≤ ε

Tactic:
lineMap_apply,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p ↦ ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y ↦ (lineMap q y) (ε / dist y q)
y : P
⊢ dist ((ε / dist y q) • (y -ᵥ q) +ᵥ q) q ≤ ε
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun i ↦ s.points ↑i -ᵥ s.centroid
h_span : ∀ (i : ↥s'), p -ᵥ s.centroid ∈ k ∙ u i
hi : LinearIndependent k u
⊢ n + 1 - #{i₀} = n

Tactic:
card_singleton,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
hn : 1 < n
p : P
h : ∀ (i : Fin (n + 1)), p ∈ s.median i
i₀ : Fin (n + 1) := 0
hp : p = (p -ᵥ s.centroid) +ᵥ s.centroid
s' : Finset (Fin (n + 1)) := {i₀}ᶜ
u : ↥s' → V := fun i ↦ s.points ↑i -ᵥ s.centroid
h_span : ∀ (i : ↥s'), p -ᵥ s.centroid ∈ k ∙ u i
hi : LinearIndependent k u
⊢ n + 1 - 1 = n
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
h : p ∈ affineSpan k s
⊢ Coplanar k (insert p s) ↔ Coplanar k s

Tactic:
Coplanar,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
h : p ∈ affineSpan k s
⊢ Module.rank k ↥(vectorSpan k (insert p s)) ≤ 2 ↔ Coplanar k s
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
h : p ∈ affineSpan k s
⊢ Module.rank k ↥(vectorSpan k (insert p s)) ≤ 2 ↔ Coplanar k s

Tactic:
Coplanar,

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
h : p ∈ affineSpan k s
⊢ Module.rank k ↥(vectorSpan k (insert p s)) ≤ 2 ↔ Module.rank k ↥(vectorSpan k s) ≤ 2
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
⊢ 0 ≤ ‖f‖

Tactic:
rcases isEmpty_or_nonempty α with _i | _i

Goal state after:
case inr.inl.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
_i : IsEmpty α
⊢ 0 ≤ ‖f‖

case inr.inl.inr
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
_i : Nonempty α
⊢ 0 ≤ ‖f‖
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
h : ‖f‖ = 0
⊢ f = 0

Tactic:
rcases isEmpty_or_nonempty α with _i | _i

Goal state after:
case inr.inl.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
h : ‖f‖ = 0
_i : IsEmpty α
⊢ f = 0

case inr.inl.inr
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
h : ‖f‖ = 0
_i : Nonempty α
⊢ f = 0