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

Goal state before:
pp: B₁ : Type u_3
B₂ : Type u_4
inst✝⁵ : CStarAlgebra B₁
inst✝⁴ : CStarAlgebra B₂
inst✝³ : PartialOrder B₁
inst✝² : PartialOrder B₂
inst✝¹ : StarOrderedRing B₁
inst✝ : StarOrderedRing B₂
f : B₁ →ₚ[ℂ] B₂
x : B₁
hx : 0 ≤ x
⊢ f x ≤ ‖x‖ • f 1

Tactic:
← Complex.coe_smul,

Goal state after:
B₁ : Type u_3
B₂ : Type u_4
inst✝⁵ : CStarAlgebra B₁
inst✝⁴ : CStarAlgebra B₂
inst✝³ : PartialOrder B₁
inst✝² : PartialOrder B₂
inst✝¹ : StarOrderedRing B₁
inst✝ : StarOrderedRing B₂
f : B₁ →ₚ[ℂ] B₂
x : B₁
hx : 0 ≤ x
⊢ f x ≤ ↑‖x‖ • f 1
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₂
hcontra : ∀ (C : ℝ≥0), ∃ a, 0 ≤ a ∧ ↑C * ‖a‖ < ‖f a‖
n : ℕ
hx₁ : 0 ≤ Classical.choose ⋯
hx₂ : ↑(2 ^ (2 * n)) * ‖Classical.choose ⋯‖ < ‖f (Classical.choose ⋯)‖
⊢ ∃ x, 0 ≤ x ∧ ‖x‖ = 1 ∧ 2 ^ (2 * n) < ‖f x‖

Tactic:
set x := Classical.choose (hcontra (2 ^ (2 * n)))

Goal state after:
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₂
hcontra : ∀ (C : ℝ≥0), ∃ a, 0 ≤ a ∧ ↑C * ‖a‖ < ‖f a‖
n : ℕ
x : A₁ := Classical.choose ⋯
hx₁ : 0 ≤ x
hx₂ : ↑(2 ^ (2 * n)) * ‖x‖ < ‖f x‖
⊢ ∃ x, 0 ≤ x ∧ ‖x‖ = 1 ∧ 2 ^ (2 * n) < ‖f x‖
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: case h₁
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝¹ m✝ : A
ε : ℝ≥0
hε : 0 < ε
x✝ : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := ⋯
hx₁ : cfc g (ε⁻¹ ^ 2 • m) ≤ x
hg : Continuous g
hg' : ContinuousOn (fun y ↦ (1 + ε⁻¹ ^ 2 • y)⁻¹) (σ ℝ≥0 m)
hx : x ∈ Set.Icc 0 1
hx' : x ∈ Set.Icc (cfc g (ε⁻¹ ^ 2 • m)) 1
this : star m * (1 - cfc g (ε⁻¹ ^ 2 • m)) * m = cfc (fun y ↦ y * (1 + ε⁻¹ ^ 2 • y)⁻¹ * y) m
y : ℝ≥0
hy : y ∈ σ ℝ≥0 m
⊢ y * ε ^ 2 ≤ ε ^ 2

pp: case h₂
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝¹ m✝ : A
ε : ℝ≥0
hε : 0 < ε
x✝ : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := ⋯
hx₁ : cfc g (ε⁻¹ ^ 2 • m) ≤ x
hg : Continuous g
hg' : ContinuousOn (fun y ↦ (1 + ε⁻¹ ^ 2 • y)⁻¹) (σ ℝ≥0 m)
hx : x ∈ Set.Icc 0 1
hx' : x ∈ Set.Icc (cfc g (ε⁻¹ ^ 2 • m)) 1
this : star m * (1 - cfc g (ε⁻¹ ^ 2 • m)) * m = cfc (fun y ↦ y * (1 + ε⁻¹ ^ 2 • y)⁻¹ * y) m
y : ℝ≥0
hy : y ∈ σ ℝ≥0 m
⊢ y / (ε ^ 2 + y) ≤ 1

Tactic:
· apply mul_le_of_le_one_left'
          have hm' := hm₂.le
          rw [norm_le_one_iff_of_nonneg m hm₁, ← cfc_id' ℝ≥0 m, ← cfc_one (R := ℝ≥0) m,
            cfc_nnreal_le_iff _ _ _ (QuasispectrumRestricts.nnreal_of_nonneg hm₁)] at hm'
          exact hm' y hy

Goal state after:
case h₂
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝¹ m✝ : A
ε : ℝ≥0
hε : 0 < ε
x✝ : A
x m : Unitization ℂ A
hm₁ : 0 ≤ m
hm₂ : ‖m‖ < 1
hx₂ : ‖x‖ ≤ 1
hx₀ : 0 ≤ x
g : ℝ≥0 → ℝ≥0 := ⋯
hx₁ : cfc g (ε⁻¹ ^ 2 • m) ≤ x
hg : Continuous g
hg' : ContinuousOn (fun y ↦ (1 + ε⁻¹ ^ 2 • y)⁻¹) (σ ℝ≥0 m)
hx : x ∈ Set.Icc 0 1
hx' : x ∈ Set.Icc (cfc g (ε⁻¹ ^ 2 • m)) 1
this : star m * (1 - cfc g (ε⁻¹ ^ 2 • m)) * m = cfc (fun y ↦ y * (1 + ε⁻¹ ^ 2 • y)⁻¹ * y) m
y : ℝ≥0
hy : y ∈ σ ℝ≥0 m
⊢ y / (ε ^ 2 + y) ≤ 1
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Projection

Goal state before:
pp: R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : Field R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
a : A
ha : p a
⊢ IsIdempotentElem a ↔ quasispectrum R a ⊆ {0, 1}

Tactic:
refine ⟨IsIdempotentElem.quasispectrum_subset R, fun h ↦ ?_⟩
  rw [IsIdempotentElem, ← cfcₙ_id' R a, ← cfcₙ_mul _ _]
  exact cfcₙ_congr fun x hx ↦ by grind

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

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝⁷ : Fintype n
inst✝⁶ : Semiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : Module R A
inst✝³ : Star A
inst✝² : NonUnitalNonAssocSemiring B
inst✝¹ : Module R B
inst✝ : Star B
f : A →⋆ₙₐ[R] B
M N : CStarMatrix n n A
⊢ (mapₗ ↑f) (M * N) = (mapₗ ↑f) M * (mapₗ ↑f) N

Tactic:
ext
    -- Un-squeezing this `simp` seems to add about half a second elaboration time.
    simp only [mapₗ_apply, map, LinearMap.coe_coe, ofMatrix_apply, mul_apply, map_sum, map_mul,
      ofMatrix_apply]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_5
inst✝¹ : Fintype m
inst✝ : NonUnitalCStarAlgebra A
M : CStarMatrix m n A
h : toCLM M = 0
i : m
j : n
⊢ M i j = 0 i j

Tactic:
zero_apply,

Goal state after:
m : Type u_1
n : Type u_2
A : Type u_5
inst✝¹ : Fintype m
inst✝ : NonUnitalCStarAlgebra A
M : CStarMatrix m n A
h : toCLM M = 0
i : m
j : n
⊢ M i j = 0
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✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedSpace 𝕜 A
inst✝⁶ : IsScalarTower 𝕜 A A
inst✝⁵ : SMulCommClass 𝕜 A A
inst✝⁴ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝³ : CompleteSpace 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
⊢ Integrable (fun x ↦ cfcₙ (f x) a) μ

Tactic:
refine integrable_cfcₙ' _ _ ⟨?_, ?_⟩ ha

Goal state after:
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✝² : 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
⊢ AEStronglyMeasurable (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ

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✝² : 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
⊢ HasFiniteIntegral (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ
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
inst✝¹ : ContinuousMap.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (spectrum ℝ ↑(ℑ a))
ha : IsStarNormal a
⊢ cfc (fun x ↦ ↑(f x.im)) a = cfc f ↑(ℑ a)

Tactic:
have : ContinuousOn (fun x ↦ (f x.re) : ℂ → ℂ) ((im · : ℂ → ℂ) '' spectrum ℂ a) := by
    rw [spectrum_imaginaryPart' a] at hf
    refine continuous_ofReal.comp_continuousOn <| hf.comp (by fun_prop) ?_
    simpa [Set.mapsTo_image_iff, Function.comp_def] using Set.mapsTo_image ..

Goal state after:
A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra ℂ A
inst✝³ : StarModule ℂ A
inst✝² : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMap.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (spectrum ℝ ↑(ℑ a))
ha : IsStarNormal a
this : ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.im) '' spectrum ℂ a)
⊢ cfc (fun x ↦ ↑(f x.im)) a = cfc f ↑(ℑ a)
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 : Set E
x : E
⊢ x ∈ extremePoints 𝕜 A ↔ x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x

Tactic:
refine ⟨fun h ↦ ⟨h.1, fun x₁ hx₁ x₂ hx₂ hx ↦ ⟨h.2 hx₁ hx₂ hx, ?_⟩⟩,
    fun h ↦ ⟨h.1, fun x₁ hx₁ x₂ hx₂ hx ↦ (h.2 x₁ hx₁ x₂ hx₂ hx).1⟩⟩
  apply h.2 hx₂ hx₁
  rwa [openSegment_symm]

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

Goal state before:
pp: case h
⊢ probChar π ≠ 1 π

Tactic:
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
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set Y
hs : IsOpen[inst✝] s
⊢ e.source ∩ ↑e ⁻¹' (ofSet s hs).source = e.source ∩ interior (↑e ⁻¹' s)

Tactic:
ofSet_source,

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set Y
hs : IsOpen[inst✝] s
⊢ e.source ∩ ↑e ⁻¹' s = e.source ∩ interior (↑e ⁻¹' s)
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: case refine_1
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.target ∩ ↑e.symm ⁻¹' s ∩ ↑e.symm ⁻¹' e'.source = e.target ∩ ↑e.symm ⁻¹' e'.source ∩ ↑e '' s

Tactic:
rw [inter_assoc, inter_assoc, inter_comm _ (e '' s), ← inter_assoc, ← inter_assoc]

Goal state after:
case refine_1
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.target ∩ ↑e.symm ⁻¹' s ∩ ↑e.symm ⁻¹' e'.source = e.target ∩ ↑e '' s ∩ ↑e.symm ⁻¹' e'.source
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: case right
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B
v : F
hx : (x, v) ∈ ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source
⊢ ↑((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)) (x, v) =
    ↑(Z.trivChange i j).toPartialEquiv (x, v)

Tactic:
simp only [trivChange, localTrivAsPartialEquiv, PartialEquiv.symm,
      Prod.mk_inj, prodMk_mem_set_prod_eq, PartialEquiv.trans_source, mem_inter_iff,
      mem_preimage, proj, mem_univ, (· ∘ ·),
      PartialEquiv.coe_trans] at hx ⊢

Goal state after:
case right
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
x : B
v : F
hx : (x ∈ Z.baseSet i ∧ True) ∧ x ∈ Z.baseSet j
⊢ True ∧ Z.coordChange (Z.indexAt x) j x (Z.coordChange i (Z.indexAt x) x v) = Z.coordChange i j x v
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
X : Type u_5
inst✝ : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt (↑e ∘ f) x
⊢ ContinuousAt f x

Tactic:
rw [e.continuousAt_iff_continuousAt_comp_left]

Goal state after:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
X : Type u_5
inst✝ : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt (↑e ∘ f) x
⊢ ContinuousAt (↑e.toOpenPartialHomeomorph ∘ f) x

B : Type u_1
F : Type u_2
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
X : Type u_5
inst✝ : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt (↑e ∘ f) x
⊢ f ⁻¹' e.source ∈ 𝓝 x
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
x y : A
⊢ -a.toProd.2 x * y = x * -a.toProd.1 y

Tactic:
simp only [neg_mul, mul_neg, central]

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
I : Type u_3
inst✝¹ : TopologicalSpace I
x : X
h : IsEvenlyCovered f x I
E' : Type u_4
inst✝ : TopologicalSpace E'
g : E' ≃ₜ E
inst : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝²] U
hfU : IsOpen[inst✝³] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
⊢ f ∘ ⇑g ⁻¹' U = ⇑g.symm '' f ⁻¹' U

Tactic:
rw [Set.preimage_comp, g.image_symm]

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

Goal state before:
pp: 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
⊢ Trivialization G f

Tactic:
have pGE (g : G) e : f (g • e) = f e := hfG.mpr ⟨g, rfl⟩
  have preim_im : f ⁻¹' f '' U = ⋃ g : G, (g • ·) ⁻¹' U := by
    ext e; refine ⟨fun ⟨e', heU, he⟩ ↦ ?_, ?_⟩
    · obtain ⟨g, rfl⟩ := hfG.mp he; exact ⟨_, ⟨g, rfl⟩, heU⟩
    · intro ⟨_, ⟨g, rfl⟩, hg⟩; exact ⟨_, hg, pGE g e⟩
  have : Nonempty (X → E) := ⟨Function.surjInv hf.surjective⟩
  refine IsOpen.trivializationDiscrete (fun g ↦ (g • ·) ⁻¹' U) (f '' U)
    ?_ (fun g W hWU ↦ ⟨fun hoW ↦ (hoW.preimage hf.continuous).inter (open_U.preimage <|
      continuous_const_smul g), fun isOpen ↦ hf.isOpen_preimage.mp ?_⟩) (fun g e₁ h₁ e₂ h₂ he ↦ ?_)
    ?_ (fun {g₁ g₂} hne ↦ disjoint_iff_inf_le.mpr fun e ⟨h₁, h₂⟩ ↦ hne <|
      mul_inv_eq_one.mp (disjoint _ ⟨_, ⟨_, h₂, ?_⟩, h₁⟩)) preim_im.subset
  · rw [← hf.isOpen_preimage, preim_im]
    exact isOpen_iUnion fun g ↦ open_U.preimage (continuous_const_smul g)
  · convert! isOpen_iUnion fun g : G ↦ isOpen.preimage (continuous_const_smul g)
    ext e; refine ⟨fun hW ↦ ?_, ?_⟩
    · have ⟨e', he', hfe⟩ := hWU hW
      obtain ⟨g', rfl⟩ := hfG.mp hfe
      refine ⟨_, ⟨g⁻¹ * g', rfl⟩, ?_, ?_⟩
      · apply Set.mem_of_eq_of_mem (pGE _ e) hW
      · apply Set.mem_of_eq_of_mem _ he'; simp_rw [mul_smul, smul_inv_smul]
    · rintro ⟨_, ⟨g, rfl⟩, hW, -⟩; apply Set.mem_of_eq_of_mem (pGE _ e).symm hW
  · rw [← pGE g, ← pGE g e₂] at he
    have ⟨g', he⟩ := hfG.mp he
    rw [← smul_left_cancel_iff g, ← he, disjoint g' ⟨_, ⟨_, h₂, he⟩, h₁⟩]
    apply one_smul
  · rintro g x ⟨e, hU, rfl⟩; exact ⟨g⁻¹ • e, by apply (smul_inv_smul g e).symm ▸ hU, pGE _ e⟩
  · simp_rw [mul_smul, inv_smul_smul]

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

Goal state before:
pp: 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₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this✝ : TopologicalSpace G := ⊥
this : DiscreteTopology G
e : E
he : e ∈ {e | MulAction.stabilizer G e = ⊥}
U : Set E
heU : U ∈ 𝓝 e
hU : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g • e = e
g : G
hg : ((fun x ↦ g • x) '' interior U ∩ interior U).Nonempty
⊢ g = 1

Tactic:
rw [← Subgroup.mem_bot, ← he]

Goal state after:
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₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this✝ : TopologicalSpace G := ⊥
this : DiscreteTopology G
e : E
he : e ∈ {e | MulAction.stabilizer G e = ⊥}
U : Set E
heU : U ∈ 𝓝 e
hU : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g • e = e
g : G
hg : ((fun x ↦ g • x) '' interior U ∩ interior U).Nonempty
⊢ g ∈ MulAction.stabilizer G e
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ 0 < x.angleDiff y

Tactic:
grind [arg_eq_arg, neg_pi_lt_arg y.val, arg_le_pi x.val]

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

Goal state before:
pp: case h
x✝ : ℝ
⊢ ↑(↑x✝).toCircle = ↑(↑x✝).cos + ↑(↑x✝).sin * I

Tactic:
simp [exp_mul_I]

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

Goal state before:
pp: case refine_1.inl
A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ ≤ π
a✝ : Nontrivial A
h : ‖↑x‖ ∈ spectrum ℝ ↑x
⊢ Real.cos ‖x‖ ∈ (fun a ↦ Real.cos a) '' spectrum ℝ ↑x

Tactic:
exact ⟨_, h, rfl⟩

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
A : E →L[𝕜] F
x : E
y : F
⊢ ⟪x, (adjointAux A) y⟫_𝕜 = ⟪A x, y⟫_𝕜

Tactic:
by
  rw [← inner_conj_symm, adjointAux_inner_left, inner_conj_symm]

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
A : E →L[𝕜] F
y : F
x : E
⊢ ‖y - A x‖ = ⨅ z, ‖y - ↑z‖ ↔ (adjoint A) (y - A x) = 0

Tactic:
by
  rw [A.range.norm_eq_iInf_iff_inner_eq_zero (by simp),
    ← Submodule.mem_orthogonal', A.orthogonal_range, LinearMap.mem_ker, coe_coe]

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
T : E →L[𝕜] E
inst✝ : CompleteSpace E
hT : IsIdempotentElem T
h : IsStarNormal T
⊢ ∀ (x : E), (T - star T * T) x = 0 x

Tactic:
zero_apply,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
hT : IsIdempotentElem T
h : IsStarNormal T
⊢ ∀ (x : E), (T - star T * T) x = 0
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
A : E →ₗ[𝕜] F
⊢ (adjoint A ∘ₗ A).kerᗮ = (adjoint A).range

Tactic:
by rw [ker_adjoint_comp_self, orthogonal_ker]

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:
rw [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.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
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
i : Fin (m + 1)
x✝ : P
⊢ x✝ ∈ (s.reindex e).median i ↔ x✝ ∈ (s.median ∘ ⇑e.symm) i

Tactic:
simp [median]

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

Goal state before:
pp: case h
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₀ ∈ s
v₀ : V
hv : ∀ v ∈ vectorSpan k s, ∃ r, r • v₀ = v
p : P
⊢ p ∈ s → ∃ r, p = r • v₀ +ᵥ p₀

Tactic:
hp

Goal state after:
case h
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₀ ∈ s
v₀ : V
hv : ∀ v ∈ vectorSpan k s, ∃ r, r • v₀ = v
p : P
hp : p ∈ s
⊢ ∃ r, p = r • v₀ +ᵥ p₀
Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases

Goal state before:
pp: case refine_1
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)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ y ∉ s, ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p ↦ if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) ⋯
p : P
⊢ p ∈ s → p ∈ range fun p ↦ (lineMap q ↑p) ↑(w p)

Tactic:
hp

Goal state after:
case refine_1
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)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ y ∉ s, ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p ↦ if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) ⋯
p : P
hp : p ∈ s
⊢ p ∈ range fun p ↦ (lineMap q ↑p) ↑(w p)
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case h
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
p₁ p₂ p : P
⊢ p ∈ {p₁, p₂} → ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁

Tactic:
hp

Goal state after:
case h
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
p₁ p₂ p : P
hp : p ∈ {p₁, p₂}
⊢ ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁