mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: case e_f.refine_2
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
i : n
⊢ ‖v i‖₊ = ‖diagonal v i i‖₊

Tactic:
diagonal_apply_eq

Goal state after:
case e_f.refine_2
n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
i : n
⊢ ‖v i‖₊ = ‖v i‖₊
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: case e_f.refine_2
m : Type u_3
α : Type u_5
inst✝² : Fintype m
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
i : m
⊢ ‖diagonal v i i‖₊ = ‖v i‖₊

Tactic:
diagonal_apply_eq

Goal state after:
case e_f.refine_2
m : Type u_3
α : Type u_5
inst✝² : Fintype m
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
i : m
⊢ ‖v i‖₊ = ‖v i‖₊
Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap

Goal state before:
pp: A₁ : Type u_1
A₂ : Type u_2
inst✝⁵ : NonUnitalCStarAlgebra A₁
inst✝⁴ : NonUnitalCStarAlgebra A₂
inst✝³ : PartialOrder A₁
inst✝² : StarOrderedRing A₁
inst✝¹ : PartialOrder A₂
inst✝ : StarOrderedRing A₂
f : A₁ →ₚ[ℂ] A₂
C : ℝ≥0
hmain : ∀ (a : A₁), 0 ≤ a → ‖f a‖ ≤ ↑C * ‖a‖
x : A₁
y : Fin 4 → A₁
hy_nonneg : ∀ (i : Fin 4), 0 ≤ y i
hy_norm : ∀ (i : Fin 4), ‖y i‖ ≤ ‖x‖
hy : x = ∑ i, I ^ ↑i • y i
⊢ ∑ i, ↑C * ‖x‖ ≤ ↑(4 * C) * ‖x‖

Tactic:
simp [mul_assoc]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
M : CStarMatrix m n A
⊢ ∑ x, ∑ x, ‖ofMatrixₗ.symm M‖ = ↑(↑(Fintype.card n) * ↑(Fintype.card m)) * ‖ofMatrixₗ.symm M‖

Tactic:
simp [mul_assoc]

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

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
⊢ (x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) → x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x

Tactic:
rw [← insert_endpoints_openSegment]

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
⊢ (x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) → x ∈ insert x₁ (insert x₂ (openSegment 𝕜 x₁ x₂)) → x₁ = x ∨ x₂ = x
Module: Mathlib.Topology.Algebra.LinearMapCompletion

Goal state before:
pp: α : Type u_1
β : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst✝¹¹ : UniformSpace α
inst✝¹⁰ : AddCommGroup α
inst✝⁹ : IsUniformAddGroup α
inst✝⁸ : Semiring R₁
inst✝⁷ : Module R₁ α
inst✝⁶ : UniformContinuousConstSMul R₁ α
inst✝⁵ : Semiring R₂
inst✝⁴ : UniformSpace β
inst✝³ : AddCommGroup β
inst✝² : IsUniformAddGroup β
inst✝¹ : Module R₂ β
inst✝ : UniformContinuousConstSMul R₂ β
σ : R₁ →+* R₂
f : α →SL[σ] β
a : α
⊢ f.completion ↑a = ↑(f a)

Tactic:
simp [coe_completion, map_coe]

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
a b : A
c : f.PreGNS
⊢ (f.leftMulMapPreGNS (a * b)) c = (f.leftMulMapPreGNS a ∘SL f.leftMulMapPreGNS b) c

Tactic:
simp [mul_assoc]

Goal state after:
Module: Mathlib.Analysis.Normed.Field.UnitBall

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
x : ↑(sphere 0 1)
⊢ ‖(↑x)⁻¹‖ = 1

Tactic:
by
    rw [norm_inv, mem_sphere_zero_iff_norm.1 x.coe_prop, inv_one]

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
⊢ (e.restr s).symm.trans e' ≈ (e.symm.trans e').restr (↑e '' s)

Tactic:
refine ⟨?_, ?_⟩
  · simp only [trans_toPartialEquiv, symm_toPartialEquiv, restr_toPartialEquiv,
      PartialEquiv.trans_source, PartialEquiv.symm_source, PartialEquiv.restr_target,
      coe_toPartialEquiv_symm, PartialEquiv.restr_coe_symm, PartialEquiv.restr_source]
    rw [interior_eq_iff_isOpen.mpr hs', interior_eq_iff_isOpen.mpr hs]
    -- Get rid of the middle term, which is merely distracting.
    rw [inter_assoc, inter_assoc, inter_comm _ (e '' s), ← inter_assoc, ← inter_assoc]
    congr 1
    -- Now, just a bunch of rewrites: should this be a separate lemma?
    rw [← image_source_inter_eq', ← image_source_eq_target]
    refine image_inter_on ?_
    intro x hx y hy h
    rw [← left_inv e hy, ← left_inv e (hs'' hx), h]
  · simp_rw [coe_trans, restr_symm_apply, restr_apply, coe_trans]
    intro x hx
    simp

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

Goal state before:
pp: case 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
⊢ ∃ e, Icc a b ⊆ e.baseSet

Tactic:
have hsb : b ∈ upperBounds s := fun x hx => hx.1.2

Goal state after:
case 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
⊢ ∃ e, Icc a b ⊆ e.baseSet
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
e e' : Pretrivialization F proj
h₁ : e.toPartialEquiv = e'.toPartialEquiv
h₂ : e.baseSet = e'.baseSet
⊢ e = e'

Tactic:
cases e

Goal state after:
case mk
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e' : Pretrivialization F proj
toPartialEquiv✝ : PartialEquiv Z (B × F)
open_target✝ : IsOpen[instTopologicalSpaceProd] toPartialEquiv✝.target
baseSet✝ : Set B
open_baseSet✝ : IsOpen[inst✝¹] baseSet✝
source_eq✝ : toPartialEquiv✝.source = proj ⁻¹' baseSet✝
target_eq✝ : toPartialEquiv✝.target = baseSet✝ ×ˢ univ
proj_toFun✝ : ∀ p ∈ toPartialEquiv✝.source, (↑toPartialEquiv✝ p).1 = proj p
h₁ :
  { toPartialEquiv := toPartialEquiv✝, open_target := open_target✝, baseSet := baseSet✝, open_baseSet := open_baseSet✝,
        source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ }.toPartialEquiv =
    e'.toPartialEquiv
h₂ :
  { toPartialEquiv := toPartialEquiv✝, open_target := open_target✝, baseSet := baseSet✝, open_baseSet := open_baseSet✝,
        source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ }.baseSet =
    e'.baseSet
⊢ { toPartialEquiv := toPartialEquiv✝, open_target := open_target✝, baseSet := baseSet✝, open_baseSet := open_baseSet✝,
      source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ } =
    e'
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b✝ : B
a : F
b : B
x : Z.Fiber b
⊢ 𝓝 x = comap (TotalSpace.mk b) (𝓝 { proj := b, snd := x })

Tactic:
rw [(Z.localTrivAt b).nhds_eq_comap_inf_principal (mk_mem_localTrivAt_source _ _ _), comap_inf,
      comap_principal, comap_comap]

Goal state after:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b✝ : B
a : F
b : B
x : Z.Fiber b
⊢ 𝓝 x =
    comap (↑(Z.localTrivAt b).toOpenPartialHomeomorph ∘ TotalSpace.mk b)
        (𝓝 (↑(Z.localTrivAt b).toOpenPartialHomeomorph { proj := b, snd := x })) ⊓
      𝓟 (TotalSpace.mk b ⁻¹' (Z.localTrivAt b).source)
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✝ : TopologicalSpace Z
e e' : Trivialization F proj
h₁ : e.toOpenPartialHomeomorph = e'.toOpenPartialHomeomorph
h₂ : e.baseSet = e'.baseSet
⊢ e = e'

Tactic:
cases e

Goal state after:
case mk
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e' : Trivialization F proj
toOpenPartialHomeomorph✝ : OpenPartialHomeomorph Z (B × F)
baseSet✝ : Set B
open_baseSet✝ : IsOpen[inst✝²] baseSet✝
source_eq✝ : toOpenPartialHomeomorph✝.source = proj ⁻¹' baseSet✝
target_eq✝ : toOpenPartialHomeomorph✝.target = baseSet✝ ×ˢ univ
proj_toFun✝ : ∀ p ∈ toOpenPartialHomeomorph✝.source, (↑toOpenPartialHomeomorph✝ p).1 = proj p
h₁ :
  { toOpenPartialHomeomorph := toOpenPartialHomeomorph✝, baseSet := baseSet✝, open_baseSet := open_baseSet✝,
        source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ }.toOpenPartialHomeomorph =
    e'.toOpenPartialHomeomorph
h₂ :
  { toOpenPartialHomeomorph := toOpenPartialHomeomorph✝, baseSet := baseSet✝, open_baseSet := open_baseSet✝,
        source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ }.baseSet =
    e'.baseSet
⊢ { toOpenPartialHomeomorph := toOpenPartialHomeomorph✝, baseSet := baseSet✝, open_baseSet := open_baseSet✝,
      source_eq := source_eq✝, target_eq := target_eq✝, proj_toFun := proj_toFun✝ } =
    e'
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: X₁ : Type u_1
X₂ : Type u_2
Y₁ : Sort u_3
Y₂ : Sort u_4
Z₁ : Type u_5
Z₂ : Type u_6
inst✝³ : TopologicalSpace X₁
inst✝² : TopologicalSpace X₂
inst✝¹ : TopologicalSpace Z₁
inst✝ : TopologicalSpace Z₂
f₁ : X₁ → Y₁
g₁ : Z₁ → Y₁
f₂ : X₂ → Y₂
g₂ : Z₂ → Y₂
mapX : X₁ → X₂
contX : Continuous[inst✝³, inst✝²] mapX
mapY : Y₁ → Y₂
mapZ : Z₁ → Z₂
contZ : Continuous[inst✝¹, inst✝] mapZ
commX : f₂ ∘ mapX = mapY ∘ f₁
commZ : g₂ ∘ mapZ = mapY ∘ g₁
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (Function.mapPullback mapX mapY mapZ commX commZ)

Tactic:
by
  refine continuous_induced_rng.mpr (.prodMk ?_ ?_) <;>
    apply_rules [continuous_fst, continuous_snd, continuous_subtype_val, Continuous.comp]

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:
rw [continuousOn_iff_continuous_domRestrict] at h₁ h₂

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.Topology.IsLocalHomeomorph

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s : Set X
x : ↑s
e : OpenPartialHomeomorph X Y
hx : ↑x ∈ e.source
h : IsLocalHomeomorphOn (↑e) s
inst✝ : DiscreteTopology ↑(↑e '' s)
U : Set Y
hU : IsOpen[inst✝¹] U
eq : Subtype.val ⁻¹' U = {⟨↑e ↑x, ⋯⟩}
x' : { x // x ∈ s }
mem : x' ∈ Subtype.val ⁻¹' (e.source ∩ ↑e ⁻¹' U)
⊢ ↑e ↑x' = ↑e ↑x

Tactic:
simpa using Set.subset_singleton_iff.1 eq.subset ⟨_, x', x'.2, rfl⟩ mem.2

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

Goal state before:
pp: 𝕜 : 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‖₊
⊢ ‖star a * a‖₊ = ‖a‖₊ * ‖a‖₊

Tactic:
rw [← nnnorm_snd]

Goal state after:
𝕜 : 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‖₊
⊢ ‖(star a * a).toProd.2‖₊ = ‖a‖₊ * ‖a‖₊
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
⊢ f x ∈ (hf.localInverseAt x).source

Tactic:
rw [← congrFun (hf.localInverseAt_symm x)]
  exact (hf.localInverseAt x).map_target hf.self_mem_localInverseAt_target

Goal state after:
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsLocalHomeomorph f
x : X
⊢ Set.InjOn f (hf.localInverseAt x).target

Tactic:
rw [Set.EqOn.injOn_iff (f₂ := (hf.localInverseAt x).symm) (fun y _ ↦ by simp)]
  exact (hf.localInverseAt x).symm.injOn

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

Goal state before:
pp: case refine_2
E : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace X
f : E → X
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G E
hf : IsQuotientMap f
inst✝² : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst✝¹ : TopologicalSpace G
inst✝ : DiscreteTopology G
U : Set E
open_U : IsOpen[inst✝⁶] U
disjoint : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ g, (fun x ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g✝ : G
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst✝⁶] (f ⁻¹' W ∩ (fun x ↦ g✝ • x) ⁻¹' U)
e : E
g : G
hW : (fun x ↦ g • x) e ∈ f ⁻¹' W
⊢ e ∈ f ⁻¹' W

Tactic:
apply Set.mem_of_eq_of_mem (pGE _ e).symm hW

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
hf : IsCoveringMap f
t : Set X
⊢ IsCoveringMap (t.restrictPreimage f)

Tactic:
isCoveringMap_iff_isCoveringMapOn_univ

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:
isCoveringMap_iff_isCoveringMapOn_univ

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:
isCoveringMap_iff_isCoveringMapOn_univ

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.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : RCLike 𝕜
p : A → Prop
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : ContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
h : Continuous ⇑(cfcHom ha)
⊢ cfc exp a = exp ((cfcHom ha) { toFun := (spectrum 𝕜 a).domRestrict id, continuous_toFun := ⋯ })

Tactic:
have _ : ContinuousOn exp (spectrum 𝕜 a) := exp_continuous.continuousOn

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : RCLike 𝕜
p : A → Prop
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : ContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
h : Continuous ⇑(cfcHom ha)
x✝ : ContinuousOn exp (spectrum 𝕜 a)
⊢ cfc exp a = exp ((cfcHom ha) { toFun := (spectrum 𝕜 a).domRestrict id, continuous_toFun := ⋯ })
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
h✝ : Nontrivial A
h_eqOn : Set.EqOn (fun z ↦ ‖z - 1‖ ^ 2) (fun z ↦ 2 * (1 - z.re)) (spectrum ℂ u)
⊢ IsGreatest ((fun z ↦ 2 * (1 - z.re)) '' spectrum ℂ u) (2 * (1 - x))

Tactic:
have : Antitone (fun y : ℝ ↦ 2 * (1 - y)) := by intro _ _ _; simp only; gcongr

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
x : ℝ
hz : IsLeast (re '' spectrum ℂ u) x
h✝ : Nontrivial A
h_eqOn : Set.EqOn (fun z ↦ ‖z - 1‖ ^ 2) (fun z ↦ 2 * (1 - z.re)) (spectrum ℂ u)
this : Antitone fun y ↦ 2 * (1 - y)
⊢ IsGreatest ((fun z ↦ 2 * (1 - z.re)) '' spectrum ℂ u) (2 * (1 - x))
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: ⊢ (Filter.map (⇑exp) (nhds 0)).HasBasis (fun x ↦ True) fun n ↦ ⇑exp '' Metric.ball 0 (π / 2 ^ (n + 1))

Tactic:
apply Filter.HasBasis.map

Goal state after:
⊢ (nhds 0).HasBasis (fun x ↦ True) fun i ↦ Metric.ball 0 (π / 2 ^ (i + 1))
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)
x✝ : A
⊢ ((mulRight R u).trans (mulRight R v)) x✝ = (mulRight R (u * v)) x✝

Tactic:
simp [mul_assoc]

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)
x : A
⊢ (mulRight R (u * v)) x = (mulRight R v) ((mulRight R u) x)

Tactic:
simp [mul_assoc]

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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
x : V
⊢ normalize x = 0 ↔ x = 0

Tactic:
by_cases hx : x = 0 <;> simp [normalize, hx]

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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
x : V
⊢ ‖x‖ • normalize x = x

Tactic:
by_cases hx : x = 0 <;> simp [normalize, hx]

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
inst✝¹ : T2Space X
inst✝ : CompactSpace E
h : IsLocalHomeomorph f
hf : Continuous[inst✝⁴, inst✝³] f
⊢ IsCoveringMap f

Tactic:
isCoveringMap_iff_isCoveringMapOn_univ

Goal state after:
E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
f : E → X
inst✝² : T2Space E
inst✝¹ : T2Space X
inst✝ : CompactSpace E
h : IsLocalHomeomorph f
hf : Continuous[inst✝⁴, inst✝³] f
⊢ IsCoveringMapOn f Set.univ
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
A : E →L[𝕜] E
hA : (↑A).IsSymmetric
⊢ adjoint A = A

Tactic:
by
  rwa [eq_comm, eq_adjoint_iff A A]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
f : E →L[𝕜] E
hf : (↑f).IsSymmetric
x✝ : E
⊢ ((innerSL 𝕜) x ∘SL f) x✝ = ((innerSL 𝕜) (f x)) x✝

Tactic:
simp [hf]

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

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : CompleteSpace F
E : Type u_5
G : Type u_6
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup G
inst✝¹ : InnerProductSpace 𝕜 G
inst✝ : CompleteSpace G
x : E
y : F
f : G →L[𝕜] F
⊢ ((rankOne 𝕜) x) y ∘SL f = ((rankOne 𝕜) x) ((adjoint f) y)

Tactic:
by
  simp_rw [rankOne_def', comp_assoc, innerSL_apply_comp]

Goal state after:
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
A : E →ₗ[𝕜] E
hA : A.IsSymmetric
⊢ adjoint A = A

Tactic:
by
  rwa [eq_comm, eq_adjoint_iff A A]

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✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
⊢ (T ∘ₗ adjoint T).IsSymmetric

Tactic:
by
  simpa using LinearMap.IsSymmetric.id.conj_adjoint T

Goal state after:
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
i : Fin (n + 1)
h1 : s.median i ≤ line[k, s.points i, s.centroid]
⊢ s.centroid ∈ line[k, s.points i, s.faceOppositeCentroid i]

Tactic:
exact centroid_mem_median s i

Goal state after:
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
h : LinearIndependent k fun i ↦ s.points ↑i -ᵥ s.points 0
x✝ : { x // x ≠ 0 }
⊢ (-↑n)⁻¹ ≠ 0

Tactic:
by simpa using NeZero.ne n

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

Goal state before:
pp: case inr
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
hp₁ : p₁ ∈ s
⊢ Collinear k s ↔ ∃ p₀ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀

Tactic:
· rw [collinear_iff_of_mem hp₁]
    constructor
    · exact fun h => ⟨p₁, h⟩
    · rintro ⟨p, v, hv⟩
      use v
      intro p₂ hp₂
      rcases hv p₂ hp₂ with ⟨r, rfl⟩
      rcases hv p₁ hp₁ with ⟨r₁, rfl⟩
      use r - r₁
      simp [vadd_vadd, ← add_smul]

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
hs : Convex ℝ s
⊢ (interior s).Nonempty ↔ affineSpan ℝ s = ⊤

Tactic:
rw [← interior_convexHull_nonempty_iff_affineSpan_eq_top, hs.convexHull_eq]

Goal state after: