mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.UniformSpace.Matrix

Goal state before:
pp: m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝ : UniformSpace 𝕜
⊢ ⨅ i, Filter.comap (fun a ↦ (a.1 i, a.2 i)) (⨅ i, Filter.comap (fun a ↦ (a.1 i, a.2 i)) (𝓤 𝕜)) =
    ⨅ i, ⨅ j, Filter.comap (fun a ↦ (a.1 i j, a.2 i j)) (𝓤 𝕜)

Tactic:
Filter.comap_iInf,

Goal state after:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝ : UniformSpace 𝕜
⊢ ⨅ i, ⨅ i_1, Filter.comap (fun a ↦ (a.1 i, a.2 i)) (Filter.comap (fun a ↦ (a.1 i_1, a.2 i_1)) (𝓤 𝕜)) =
    ⨅ i, ⨅ j, Filter.comap (fun a ↦ (a.1 i j, a.2 i j)) (𝓤 𝕜)
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_2
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ c ^ 2
⊢ ‖z - y * z‖₊ ≤ c

Tactic:
← one_mul z

Goal state after:
A : Type u_2
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hy : y ∈ Set.Icc x 1
c : ℝ≥0
h : ‖star z * (1 - x) * z‖₊ ≤ c ^ 2
⊢ ‖1 * z - y * z‖₊ ≤ c
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: case neg
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : IsScalarTower 𝕜 A A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : ContinuousStar A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
hf : ContinuousOn f s
hf0 : f 0 = 0
hs0 : 0 ∉ s
⊢ ContinuousOn (fun x ↦ cfcₙ f x) {a | p a ∧ quasispectrum 𝕜 a ⊆ s}

Tactic:
· convert! continuousOn_empty _
    rw [Set.eq_empty_iff_forall_notMem]
    exact fun a ha ↦ hs0 <| ha.2 <| quasispectrum.zero_mem 𝕜 a

Goal state after:
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
ha : IsStarNormal a
⊢ spectrum ℝ ↑(ℜ a) = re '' spectrum ℂ a

Tactic:
simp [← (ℜ a).2.spectrumRestricts.image, spectrum_realPart a, Set.image_image]

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

Goal state before:
pp: ι : Type u_1
E : Type u_2
inst✝² : Fintype ι
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
b : OrthonormalBasis ι ℝ E
L : StrongDual ℝ E
this : FiniteDimensional ℝ E
⊢ ‖L‖ ^ 2 = ∑ i, L (b i) ^ 2

Tactic:
← (InnerProductSpace.toDual ℝ E).symm.norm_map,

Goal state after:
ι : Type u_1
E : Type u_2
inst✝² : Fintype ι
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
b : OrthonormalBasis ι ℝ E
L : StrongDual ℝ E
this : FiniteDimensional ℝ E
⊢ ‖(InnerProductSpace.toDual ℝ E).symm L‖ ^ 2 = ∑ i, L (b i) ^ 2
Module: Mathlib.Analysis.CStarAlgebra.Extreme

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
e : A
x✝ :
  (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
⊢ ↑e * (2 - ↑e) = ↑(2 • e - e * e)

Tactic:
simp [mul_sub, two_smul, mul_two]

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

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Y'
eX eX' : OpenPartialHomeomorph X X'
eY eY' : OpenPartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
x : X
y : Y
this✝² : Nonempty X
this✝¹ : Nonempty X'
this✝ : Nonempty Y
this : Nonempty Y'
⊢ (∀ (x : X × Y), ↑eX x.1 = ↑eX' x.1 ∧ ↑eY x.2 = ↑eY' x.2) ∧
      (∀ (x : X' × Y'), ↑eX.symm x.1 = ↑eX'.symm x.1 ∧ ↑eY.symm x.2 = ↑eY'.symm x.2) ∧
        eX.source = eX'.source ∧ eY.source = eY'.source ↔
    ((∀ (x : X), ↑eX x = ↑eX' x) ∧ (∀ (x : X'), ↑eX.symm x = ↑eX'.symm x) ∧ eX.source = eX'.source) ∧
      (∀ (x : Y), ↑eY x = ↑eY' x) ∧ (∀ (x : Y'), ↑eY.symm x = ↑eY'.symm x) ∧ eY.source = eY'.source

Tactic:
forall_and,

Goal state after:
X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Y'
eX eX' : OpenPartialHomeomorph X X'
eY eY' : OpenPartialHomeomorph Y Y'
h : (eX.prod eY).source.Nonempty
x : X
y : Y
this✝² : Nonempty X
this✝¹ : Nonempty X'
this✝ : Nonempty Y
this : Nonempty Y'
⊢ ((∀ (x : X × Y), ↑eX x.1 = ↑eX' x.1) ∧ ∀ (x : X × Y), ↑eY x.2 = ↑eY' x.2) ∧
      ((∀ (x : X' × Y'), ↑eX.symm x.1 = ↑eX'.symm x.1) ∧ ∀ (x : X' × Y'), ↑eY.symm x.2 = ↑eY'.symm x.2) ∧
        eX.source = eX'.source ∧ eY.source = eY'.source ↔
    ((∀ (x : X), ↑eX x = ↑eX' x) ∧ (∀ (x : X'), ↑eX.symm x = ↑eX'.symm x) ∧ eX.source = eX'.source) ∧
      (∀ (x : Y), ↑eY x = ↑eY' x) ∧ (∀ (x : Y'), ↑eY.symm x = ↑eY'.symm x) ∧ eY.source = eY'.source
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Opens X
hs : Nonempty ↥s
x : ↥s
hxe : ↑x ∈ e.source
⊢ ↑e ↑x ∈ (e.subtypeRestr hs).target

Tactic:
refine ⟨e.map_source hxe, ?_⟩
  rw [s.openPartialHomeomorphSubtypeCoe_target, mem_preimage, e.leftInvOn hxe]
  exact x.prop

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

Goal state before:
pp: case pos
B : Type u_2
F : Type u_3
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
d : B
hdcb : d ∈ Ioc c b
hd : Ico c d ⊆ ec.baseSet
had : Ico a d ⊆ ec.baseSet
he : Disjoint (Iio d) (Ioi c)
ed : Trivialization F TotalSpace.proj
hed : d ∈ ed.baseSet
x : B
hx : x ∈ Icc a d
⊢ x ∈ ((ec.restrOpen (Iio d) ⋯).disjointUnion (ed.restrOpen (Ioi c) ⋯) ⋯).baseSet

Tactic:
rcases hx.2.eq_or_lt with (rfl | hxd)

Goal state after:
case pos.inl
B : Type u_2
F : Type u_3
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
ed : Trivialization F TotalSpace.proj
x : B
hdcb : x ∈ Ioc c b
hd : Ico c x ⊆ ec.baseSet
had : Ico a x ⊆ ec.baseSet
he : Disjoint (Iio x) (Ioi c)
hed : x ∈ ed.baseSet
hx : x ∈ Icc a x
⊢ x ∈ ((ec.restrOpen (Iio x) ⋯).disjointUnion (ed.restrOpen (Ioi c) ⋯) ⋯).baseSet

case pos.inr
B : Type u_2
F : Type u_3
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
d : B
hdcb : d ∈ Ioc c b
hd : Ico c d ⊆ ec.baseSet
had : Ico a d ⊆ ec.baseSet
he : Disjoint (Iio d) (Ioi c)
ed : Trivialization F TotalSpace.proj
hed : d ∈ ed.baseSet
x : B
hx : x ∈ Icc a d
hxd : x < d
⊢ x ∈ ((ec.restrOpen (Iio d) ⋯).disjointUnion (ed.restrOpen (Ioi c) ⋯) ⋯).baseSet
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: X : Type u_1
Y : Sort u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
sep : IsSeparatedMap f
g : A → Y
⊢ IsSeparatedMap snd

Tactic:
isSeparatedMap_iff_isClosed_diagonal

Goal state after:
X : Type u_1
Y : Sort u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
sep : IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)
g : A → Y
⊢ IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal snd)
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: X : Type u_1
Y : Sort u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
sep : IsSeparatedMap f
g : A → X
cont : Continuous[inst✝, inst✝¹] g
inj : Function.Injective g
⊢ IsSeparatedMap (f ∘ g)

Tactic:
isSeparatedMap_iff_isClosed_diagonal

Goal state after:
X : Type u_1
Y : Sort u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
sep : IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)
g : A → X
cont : Continuous[inst✝, inst✝¹] g
inj : Function.Injective g
⊢ IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal (f ∘ g))
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
s : Set X
F : ↑s → Type u_3
inst✝ : (x : ↑s) → TopologicalSpace (F x)
hF : ∀ (x : ↑s), DiscreteTopology (F x)
e : (x : ↑s) → Trivialization (F x) f
h : ∀ (x : ↑s), ↑x ∈ (e x).baseSet
⊢ IsCoveringMapOn f s

Tactic:
cases isEmpty_or_nonempty E
  · exact .of_isEmpty _ _
  refine .mk' _ _ _ (fun x _ ↦ ⟨e x, h x⟩) fun x hx ↦ (hx ?_).elim
  exact ⟨(e x).invFun (x, (e x <| Classical.arbitrary E).2), (e x).proj_symm_apply' (h x)⟩

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

Goal state before:
pp: case refine_1.a
E : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace X
f : E → X
s : Set X
inst✝³ : Nonempty (X → E)
ι : Type ?u.20
inst✝² : Nonempty ι
inst✝¹ : TopologicalSpace ι
inst✝ : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst✝⁴] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst✝⁴] W ↔ IsOpen[inst✝⁵] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ i, U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : ι → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
F : PartialEquiv E (X × ι) :=
  { toFun := fun e ↦ (f e, if he : f e ∈ V then idx e he else Classical.arbitrary ι),
    invFun := fun x ↦ if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1, source := f ⁻¹' V,
    target := V ×ˢ Set.univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }
open_preim : ∀ {W : Set X}, W ⊆ V → IsOpen[inst✝⁴] W → IsOpen[inst✝⁵] (f ⁻¹' W)
open_source : IsOpen[inst✝⁵] F.source
cont_f : ContinuousOn f F.source
e : E
he : e ∈ F.source
e' : E
he' : e' ∈ U (idx e he) ∩ F.source
h : e' ∉ {x | (fun x ↦ (fun x ↦ idx e he) x = (fun x ↦ if he : f x ∈ V then idx x he else Classical.arbitrary ι) x) x}
⊢ ?refine_1.a✝ ∈ U (idx e he) ⊓ U (idx e' ⋯)

Tactic:
exact ⟨he'.1, idx_U ..⟩

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : IsStrictlyPositive a
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
| a

Tactic:
rw [← cfc_id (R := ℝ) a]

Goal state after:
A : Type u_1
inst✝⁶ : NormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedAlgebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : IsStrictlyPositive a
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
| cfc id a
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ range ⇑(x.path y) ∪ range ⇑(y.path x) = univ

Tactic:
by
  rw [range_path, range_path, ← image_union, Icc_union_Icc_angleDiff_add_arg h,
    periodic_exp.image_Icc two_pi_pos]
  exact exp_surjective.range_eq

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
s : Set X
inst✝³ : Nonempty (X → E)
ι : Type ?u.20
inst✝² : Nonempty ι
inst✝¹ : TopologicalSpace ι
inst✝ : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst✝⁴] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst✝⁴] W ↔ IsOpen[inst✝⁵] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ i, U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : ι → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
⊢ Trivialization ι f

Tactic:
let F : PartialEquiv E (X × ι) :=
  { toFun e := (f e, if he : f e ∈ V then idx e he else Classical.arbitrary ι),
    invFun x := if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1,
    source := f ⁻¹' V,
    target := V ×ˢ Set.univ,
    map_source' x hx := ⟨hx, ⟨⟩⟩
    map_target' x hx := by rw [dif_pos hx.1]; apply (f_inv _ hx.1).symm ▸ hx.1,
    left_inv' e he := by
      simp_rw [dif_pos (id he : f e ∈ V)]
      exact inj _ (inv_U _ he) (idx_U e he) (f_inv _ _)
    right_inv' x hx := by
      rw [dif_pos hx.1]
      refine Prod.ext (f_inv _ hx.1) ?_
      rw [dif_pos ((f_inv _ hx.1).symm ▸ hx.1)]
      by_contra h; exact (disjoint h).le_bot ⟨idx_U .., inv_U _ _⟩ }
  have open_preim {W} (hWV : W ⊆ V) (open_W : IsOpen W) : IsOpen (f ⁻¹' W) := by
    convert! isOpen_iUnion (fun i ↦ (open_iff i hWV).mp open_W)
    rw [← Set.inter_iUnion, eq_comm, Set.inter_eq_left]
    exact (Set.preimage_mono hWV).trans exhaustive'
  have open_source : IsOpen F.source := open_preim subset_rfl open_V
  have cont_f : ContinuousOn f F.source := (continuousOn_open_iff open_source).mpr
    fun W open_W ↦ open_preim Set.inter_subset_left (open_V.inter open_W)
  refine
  { toPartialEquiv := F,
    open_source := open_source,
    open_target := open_V.prod isOpen_univ,
    continuousOn_toFun := cont_f.prodMk <| continuousOn_of_forall_continuousAt fun e he ↦
      continuous_const (y := idx e he) |>.continuousAt.congr <| mem_nhds_iff.mpr
        ⟨U (idx e he) ∩ F.source, fun e' he' ↦ ?_, ?_, idx_U e he, he⟩
    continuousOn_invFun := continuousOn_prod_of_discrete_right.mpr fun i ↦ ?_,
    baseSet := V,
    open_baseSet := open_V,
    source_eq := rfl,
    target_eq := rfl,
    proj_toFun _ _ := rfl }
  · by_contra h; apply (disjoint h).le_bot
    · dsimp only; rw [dif_pos (by exact he'.2)]; exact ⟨he'.1, idx_U ..⟩
  · rwa [Set.inter_comm, ← open_iff _ subset_rfl]
  · simp_rw [F, Set.prodMk_mem_set_prod_eq, Set.mem_univ, and_true]
    refine (continuousOn_open_iff open_V).mpr fun W open_W ↦ ?_
    rw [open_iff i Set.inter_subset_left]
    convert! ((open_iff i subset_rfl).mp open_V).inter open_W using 1
    refine Set.ext fun e ↦ and_right_comm.trans (and_congr_right fun ⟨hV, hU⟩ ↦ ?_)
    rw [Set.mem_preimage, dif_pos hV, inj i (inv_U i _) hU (f_inv i _)]

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

Goal state before:
pp: n : ℤ
inst✝ : NeZero n
⊢ IsQuotientCoveringMap (fun x ↦ x ^ n) ↥(zpowGroupHom n).ker

Tactic:
have hn : IsUnit (n : ℝ) := by simpa using NeZero.ne n

Goal state after:
n : ℤ
inst✝ : NeZero n
hn : IsUnit ↑n
⊢ IsQuotientCoveringMap (fun x ↦ x ^ n) ↥(zpowGroupHom n).ker
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
T : E →L[𝕜] E
hT : IsSelfAdjoint T
S : E →L[𝕜] F
⊢ IsSelfAdjoint (S ∘SL T ∘SL adjoint S)

Tactic:
by
  rw [isSelfAdjoint_iff'] at hT ⊢
  simp only [hT, adjoint_comp, adjoint_adjoint]
  exact ContinuousLinearMap.comp_assoc _ _ _

Goal state after:
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
T : E →L[𝕜] E
hT : IsSelfAdjoint T
S : F →L[𝕜] E
⊢ IsSelfAdjoint (adjoint S ∘SL T ∘SL S)

Tactic:
by
  rw [isSelfAdjoint_iff'] at hT ⊢
  simp only [hT, adjoint_comp, adjoint_adjoint]
  exact ContinuousLinearMap.comp_assoc _ _ _

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

Goal state before:
pp: case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑s ⊆ ↑(affineSpan k ↑t)
hs' : s.Nonempty
ht' : t.Nonempty
this✝ : Nonempty ↥s
this : Nonempty ↑↑t
direction_le : vectorSpan k (Set.range Subtype.val) ≤ vectorSpan k (Set.range Subtype.val)
finrank_le :
  finrank k ↥(vectorSpan k (Set.range Subtype.val)) + 1 ≤ finrank k ↥(vectorSpan k (Set.range Subtype.val)) + 1
⊢ #s ≤ #t

Tactic:
hs.finrank_vectorSpan_add_one

Goal state after:
case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑s ⊆ ↑(affineSpan k ↑t)
hs' : s.Nonempty
ht' : t.Nonempty
this✝ : Nonempty ↥s
this : Nonempty ↑↑t
direction_le : vectorSpan k (Set.range Subtype.val) ≤ vectorSpan k (Set.range Subtype.val)
finrank_le : Fintype.card ↥s ≤ finrank k ↥(vectorSpan k (Set.range Subtype.val)) + 1
⊢ #s ≤ #t
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : affineSpan k ↑s < affineSpan k ↑t
hs' : s.Nonempty
ht' : t.Nonempty
this✝ : Nonempty ↥s
this : Nonempty ↑↑t
dir_lt : vectorSpan k (Set.range Subtype.val) < vectorSpan k (Set.range Subtype.val)
finrank_lt :
  finrank k ↥(vectorSpan k (Set.range Subtype.val)) + 1 < finrank k ↥(vectorSpan k (Set.range Subtype.val)) + 1
⊢ #s < #t

Tactic:
hs.finrank_vectorSpan_add_one

Goal state after:
case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : affineSpan k ↑s < affineSpan k ↑t
hs' : s.Nonempty
ht' : t.Nonempty
this✝ : Nonempty ↥s
this : Nonempty ↑↑t
dir_lt : vectorSpan k (Set.range Subtype.val) < vectorSpan k (Set.range Subtype.val)
finrank_lt : Fintype.card ↥s < finrank k ↥(vectorSpan k (Set.range Subtype.val)) + 1
⊢ #s < #t
Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases

Goal state before:
pp: case inr
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
⊢ interior ((convexHull ℝ) (range ⇑b)) = {x | ∀ (i : ι), 0 < (b.coord i) x}

Tactic:
have : FiniteDimensional ℝ E := b.finiteDimensional
    have : convexHull ℝ (range b) = ⋂ i, b.coord i ⁻¹' Ici 0 := by
      rw [b.convexHull_eq_nonneg_coord, ofPred_forall]; rfl
    ext
    simp only [this, interior_iInter_of_finite, ←
      IsOpenMap.preimage_interior_eq_interior_preimage (isOpenMap_barycentric_coord b _)
        (continuous_barycentric_coord b _),
      interior_Ici, mem_iInter, mem_ofPred_eq, mem_Ioi, mem_preimage]

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ⇑b = Subtype.val
this : (interior ((convexHull ℝ) t)).Nonempty
⊢ (interior ((convexHull ℝ) s)).Nonempty

Tactic:
refine this.mono (by gcongr)

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

Goal state before:
pp: case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ Memℓp 0 0

pp: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ Memℓp 0 ∞

pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
⊢ Memℓp 0 p

Tactic:
· apply memℓp_zero
    simp

Goal state after:
case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ Memℓp 0 ∞

case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
⊢ Memℓp 0 p
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 g : (i : α) → E i
hf : Memℓp f ∞
hg : Memℓp g ∞
A : ℝ
hA : A ∈ upperBounds (Set.range fun i ↦ ‖f i‖)
B : ℝ
hB : B ∈ upperBounds (Set.range fun i ↦ ‖g i‖)
i : α
⊢ (fun i ↦ ‖(f + g) i‖) i ≤ A + B

Tactic:
exact le_trans (norm_add_le _ _) (add_le_add (hA ⟨i, rfl⟩) (hB ⟨i, rfl⟩))

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

Goal state before:
pp: case inr.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp f p
c : 𝕜
hp : 0 < p.toReal
⊢ Summable fun i ↦ ‖c • f i‖ ^ p.toReal

Tactic:
have := (hf.summable hp).mul_left (↑(‖c‖₊ ^ p.toReal) : ℝ)

Goal state after:
case inr.inr
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp f p
c : 𝕜
hp : 0 < p.toReal
this : Summable fun i ↦ ↑(‖c‖₊ ^ p.toReal) * ‖f i‖ ^ p.toReal
⊢ Summable fun i ↦ ‖c • f i‖ ^ p.toReal
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
hf₁ : ∀ (i : α), 0 ≤ ‖↑f i‖
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖

Tactic:
have hg₁ : ∀ i, 0 ≤ ‖g i‖ := fun i => norm_nonneg _

Goal state after:
case inr
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
hf₁ : ∀ (i : α), 0 ≤ ‖↑f i‖
hg₁ : ∀ (i : α), 0 ≤ ‖↑g i‖
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
hpq : p.toReal.HolderConjugate q.toReal
f : ↥(lp E p)
g : ↥(lp E q)
hf₁ : ∀ (i : α), 0 ≤ ‖↑f i‖
⊢ (Summable fun i ↦ ‖↑f i‖ * ‖↑g i‖) ∧ ∑' (i : α), ‖↑f i‖ * ‖↑g i‖ ≤ ‖f‖ * ‖g‖

Tactic:
have hg₁ : ∀ i, 0 ≤ ‖g i‖ := fun i => norm_nonneg _

Goal state after:
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
hpq : p.toReal.HolderConjugate q.toReal
f : ↥(lp E p)
g : ↥(lp E q)
hf₁ : ∀ (i : α), 0 ≤ ‖↑f i‖
hg₁ : ∀ (i : α), 0 ≤ ‖↑g i‖
⊢ (Summable fun i ↦ ‖↑f i‖ * ‖↑g i‖) ∧ ∑' (i : α), ‖↑f i‖ * ‖↑g i‖ ≤ ‖f‖ * ‖g‖
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case top.refine_1.inl
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : 0 < ∞
⊢ ‖Pi.single i x i‖ ≤ ‖x‖

Tactic:
rw [Pi.single_eq_same]

Goal state after: