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

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

Tactic:
simp only [approx]
    rw [ihn, ihn, midpoint_self]
    exacts [hx, fun hU => hx <| c.left_U_subset hU]

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

Goal state before:
pp: k : Type u_1
E : Type u_2
inst✝⁸ : Ring k
inst✝⁷ : PartialOrder k
inst✝⁶ : IsOrderedRing k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
a b : E
r r' : k
inst✝ : PosSMulReflectLT k E
h : r < r'
⊢ (1 - r) • a < (1 - r') • a + (r' • b - r • b) ↔ a < b

Tactic:
← sub_lt_iff_lt_add',

Goal state after:
k : Type u_1
E : Type u_2
inst✝⁸ : Ring k
inst✝⁷ : PartialOrder k
inst✝⁶ : IsOrderedRing k
inst✝⁵ : AddCommGroup E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : Module k E
inst✝¹ : IsStrictOrderedModule k E
a b : E
r r' : k
inst✝ : PosSMulReflectLT k E
h : r < r'
⊢ (1 - r) • a - (1 - r') • a < r' • b - r • b ↔ a < b
Module: Mathlib.Analysis.Normed.Module.WeakDual

Goal state before:
pp: 𝕜 : Type u_1
M : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : Module 𝕜 M
s : Set M
⊢ IsClosed (⋂ i ∈ s, {x | ‖x i‖ ≤ 1})

Tactic:
exact isClosed_biInter fun x hx => isClosed_Iic.preimage (WeakBilin.eval_continuous _ _).norm

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

Goal state before:
pp: A : Type u_1
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarRing A
inst✝¹ : TopologicalSpace A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
⊢ 0⁻ = 0

Tactic:
simp [negPart_def]

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
hb₂ : SpectrumRestricts b ⇑ContinuousMap.realToNNReal
⊢ ‖(algebraMap ℝ A) ↑(‖a‖₊ + ‖b‖₊) - (a + b)‖₊ ≤ ‖a‖₊ + ‖b‖₊

Tactic:
NNReal.coe_add,

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
a b : A
ha₁ : IsSelfAdjoint a
hb₁ : IsSelfAdjoint b
ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
hb₂ : SpectrumRestricts b ⇑ContinuousMap.realToNNReal
⊢ ‖(algebraMap ℝ A) (↑‖a‖₊ + ↑‖b‖₊) - (a + b)‖₊ ≤ ‖a‖₊ + ‖b‖₊
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric

Goal state before:
pp: case inl
A : Type u_1
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace ℝ A
inst✝³ : SMulCommClass ℝ A A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : StarRing A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
x : ℝ
hx : x ∈ quasispectrum ℝ a
hx' : 0 ≤ x
⊢ ‖x‖ ≤ max ‖a⁺‖ ‖a⁻‖

Tactic:
apply le_max_of_le_left
    refine le_of_eq_of_le ?_ <| norm_apply_le_norm_cfcₙ _ a hx
    rw [posPart_eq_self.mpr hx']

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

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

Tactic:
rpow_rpow_of_exponent_nonneg _ _ _ (by simp) h₁,

Goal state after:
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
ha : 0 ≤ a
hx : ¬x = 0
h₁ : 0 ≤ ↑x
⊢ a ^ (1 / 2 * ↑x) = a ^ (↑x / 2)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : StarOrderedRing A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
a✝ : Nontrivial A
h : IsStrictlyPositive a⁻¹ʳ
ha : IsUnit a
⊢ IsStrictlyPositive a

Tactic:
rw [← Ring.inverse_inverse ha]

Goal state after:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : StarOrderedRing A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
a✝ : Nontrivial A
h : IsStrictlyPositive a⁻¹ʳ
ha : IsUnit a
⊢ IsStrictlyPositive a⁻¹ʳ⁻¹ʳ
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a e : A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
this : a * e = a
⊢ e * a = a

Tactic:
simpa [ha.star_eq, he.isSelfAdjoint.star_eq] using congr(star $this)

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

Goal state before:
pp: A : Type u_1
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℂ E
⊢ ∀ {z : ℂ} {x y : E}, ⟪x, z • y⟫_ℂ = z • ⟪x, y⟫_ℂ

Tactic:
simp [inner_smul_right, smul_eq_mul]

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

Goal state before:
pp: case refine_1
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun x ↦ m * x) l (𝓝 m)
m : A
⊢ Tendsto (fun x ↦ x * m) l (𝓝 m)

Tactic:
apply (star_star m ▸ (continuous_star.tendsto _ |>.comp <| h (star m))).congr'

Goal state after:
case refine_1
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun x ↦ m * x) l (𝓝 m)
m : A
⊢ (star ∘ fun x ↦ star m * x) =ᶠ[l] fun x ↦ x * m
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: case refine_2
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun x ↦ x * m) l (𝓝 m)
m : A
⊢ Tendsto (fun x ↦ m * x) l (𝓝 m)

Tactic:
apply (star_star m ▸ (continuous_star.tendsto _ |>.comp <| h (star m))).congr'

Goal state after:
case refine_2
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
h : ∀ (m : A), Tendsto (fun x ↦ x * m) l (𝓝 m)
m : A
⊢ (star ∘ fun x ↦ x * star m) =ᶠ[l] fun x ↦ m * x
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: α : Type u_5
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
⊢ a * unitOf a = (algebraMap ℝ α) ↑‖a‖₊

Tactic:
simp only [unitOf, coe_nnnorm]

Goal state after:
α : Type u_5
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
⊢ (a * if a = 0 then 1 else ‖a‖ • a⁻¹) = (algebraMap ℝ α) ‖a‖
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: n : Type u_4
α : Type u_5
ι : Type u_7
inst✝² : Fintype n
inst✝¹ : Unique ι
inst✝ : SeminormedAddCommGroup α
v : n → α
⊢ ‖replicateCol ι v‖ = ‖toLp 2 v‖

Tactic:
simp [frobenius_norm_def, PiLp.norm_eq_of_L2, Real.sqrt_eq_rpow]

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

Goal state before:
pp: l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : RCLike α
A : Matrix l m α
B : Matrix m n α
⊢ (∑ i, ∑ j, ‖∑ j_1, A i j_1 * B j_1 j‖₊ ^ 2) ^ (1 / 2) ≤ (∑ i, ∑ j, (∑ j, ‖A i j‖₊ ^ 2) * ∑ x, ‖B x j‖₊ ^ 2) ^ (1 / 2)

Tactic:
gcongr with i _ j

Goal state after:
case h
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : RCLike α
A : Matrix l m α
B : Matrix m n α
i : l
a✝¹ : i ∈ Finset.univ
j : n
a✝ : j ∈ Finset.univ
⊢ ‖∑ j_1, A i j_1 * B j_1 j‖₊ ^ 2 ≤ (∑ j, ‖A i j‖₊ ^ 2) * ∑ x, ‖B x j‖₊ ^ 2
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
A : Matrix m n 𝕜
⊢ ‖Aᴴ‖ = ‖A‖

Tactic:
l2_opNorm_def,

Goal state after:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
A : Matrix m n 𝕜
⊢ ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) Aᴴ‖ = ‖A‖
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m n 𝕜
⊢ ‖Aᴴ * A‖ = ‖A‖ * ‖A‖

Tactic:
l2_opNorm_def,

Goal state after:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m n 𝕜
⊢ ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) (Aᴴ * A)‖ = ‖A‖ * ‖A‖
Module: Mathlib.Analysis.Complex.Circle

Goal state before:
pp: E : Type u_4
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℂ E
u : Circle
v : E
⊢ ‖u • v‖ = ‖v‖

Tactic:
by
  rw [smul_def, norm_smul, norm_eq_of_mem_sphere, one_mul]

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
i : n
⊢ ‖v i‖ ≤ ‖T‖

Tactic:
calc _ = ‖T (toLp 2 (Pi.single i (1 : 𝕜)))‖ := by
          rw [toEuclideanCLM_toLp (diagonal v) (Pi.single i (1 : 𝕜))]
          simp
      _ ≤ _ := by grw [T.le_opNorm]; simp

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

Goal state before:
pp: 𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
E : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
r : 𝕜
x : Matrix m n 𝕜
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
l2_opNorm_def,

Goal state after:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
E : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
r : 𝕜
x : Matrix m n 𝕜
⊢ ‖(toEuclideanLin ≪≫ₗ toContinuousLinearMap) (r • x)‖ ≤ ‖r‖ * ‖x‖
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
m : Type u_2
n : Type u_3
l : Type u_4
E : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
r : 𝕜
x : Matrix m n 𝕜
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
rw [l2_opNorm_def, map_smul]
    exact norm_smul_le r ((toEuclideanLin (𝕜 := 𝕜) (m := m) (n := n)).trans toContinuousLinearMap x)

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
Z : Type u_5
Z' : Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : X ≃ₜ Y
e' : Y ≃ₜ Z
f'' : OpenPartialHomeomorph Z Z'
⊢ (e.trans e').transOpenPartialHomeomorph f'' = e.transOpenPartialHomeomorph (e'.transOpenPartialHomeomorph f'')

Tactic:
by
  simp only [transOpenPartialHomeomorph_eq_trans, OpenPartialHomeomorph.trans_assoc,
    trans_toOpenPartialHomeomorph]

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

Goal state before:
pp: 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}
⊢ Icc a a ⊆ ea.baseSet

Tactic:
by simp [hea]

Goal state after:
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
i : ι
⊢ ContinuousOn (↑(Z.localTrivAsPartialEquiv i)) (Z.localTrivAsPartialEquiv i).source

Tactic:
rw [continuousOn_open_iff (Z.open_source' i)]
    intro s s_open
    apply TopologicalSpace.GenerateOpen.basic
    simp only [exists_prop, mem_iUnion, mem_singleton_iff]
    exact ⟨i, s, s_open, rfl⟩

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

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

Tactic:
by simpa using ⟨(e.invFun x).2, e.map_target hx⟩

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

Goal state before:
pp: case refine_1
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x
⊢ (have this := fun x ↦ { proj := x, snd := v };
      this) ⁻¹'
      (Z.localTrivAt x).source ∈
    𝓝 x

Tactic:
exact A

Goal state after:
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:
refine continuous_induced_rng.mpr (.prodMk ?_ ?_) <;>
    apply_rules [continuous_fst, continuous_snd, continuous_subtype_val, Continuous.comp]

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
J : Type u_4
inst✝ : TopologicalSpace J
g : I ≃ₜ J
x : X
h : IsEvenlyCovered f x I
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
x✝ : ↑(f ⁻¹' U)
⊢ ↑((H.trans ((Homeomorph.refl ↑U).prodCongr g)) x✝).1 = f ↑x✝

Tactic:
simp [hH]

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
e₁ : E
hf : IsEvenlyCovered f (f e₁) ↑(f ⁻¹' {f e₁})
e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this✝ : Nonempty ↑(f ⁻¹' {f e₁})
t : Trivialization (↑(f ⁻¹' {f e₁})) f := hf.toTrivialization
this : DiscreteTopology ↑(f ⁻¹' {f e₁})
he₁ : e₁ ∈ t.source
he₂ : e₂ ∈ t.source
⊢ ∃ s₁ s₂, IsOpen[inst✝¹] s₁ ∧ IsOpen[inst✝¹] s₂ ∧ e₁ ∈ s₁ ∧ e₂ ∈ s₂ ∧ Disjoint s₁ s₂

Tactic:
refine ⟨t.source ∩ (Prod.snd ∘ t) ⁻¹' {(t e₁).2}, t.source ∩ (Prod.snd ∘ t) ⁻¹' {(t e₂).2},
      ?_, ?_, ⟨he₁, rfl⟩, ⟨he₂, rfl⟩, Set.disjoint_left.mpr fun x h₁ h₂ ↦ hne (t.injOn he₁ he₂ ?_)⟩

Goal state after:
case refine_1
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
e₁ : E
hf : IsEvenlyCovered f (f e₁) ↑(f ⁻¹' {f e₁})
e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this✝ : Nonempty ↑(f ⁻¹' {f e₁})
t : Trivialization (↑(f ⁻¹' {f e₁})) f := hf.toTrivialization
this : DiscreteTopology ↑(f ⁻¹' {f e₁})
he₁ : e₁ ∈ t.source
he₂ : e₂ ∈ t.source
⊢ IsOpen[inst✝¹] (t.source ∩ Prod.snd ∘ ↑t ⁻¹' {(↑t e₁).2})

case refine_2
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
e₁ : E
hf : IsEvenlyCovered f (f e₁) ↑(f ⁻¹' {f e₁})
e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this✝ : Nonempty ↑(f ⁻¹' {f e₁})
t : Trivialization (↑(f ⁻¹' {f e₁})) f := hf.toTrivialization
this : DiscreteTopology ↑(f ⁻¹' {f e₁})
he₁ : e₁ ∈ t.source
he₂ : e₂ ∈ t.source
⊢ IsOpen[inst✝¹] (t.source ∩ Prod.snd ∘ ↑t ⁻¹' {(↑t e₂).2})

case refine_3
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
e₁ : E
hf : IsEvenlyCovered f (f e₁) ↑(f ⁻¹' {f e₁})
e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this✝ : Nonempty ↑(f ⁻¹' {f e₁})
t : Trivialization (↑(f ⁻¹' {f e₁})) f := hf.toTrivialization
this : DiscreteTopology ↑(f ⁻¹' {f e₁})
he₁ : e₁ ∈ t.source
he₂ : e₂ ∈ t.source
x : E
h₁ : x ∈ t.source ∩ Prod.snd ∘ ↑t ⁻¹' {(↑t e₁).2}
h₂ : x ∈ t.source ∩ Prod.snd ∘ ↑t ⁻¹' {(↑t e₂).2}
⊢ ↑t.toOpenPartialHomeomorph e₁ = ↑t.toOpenPartialHomeomorph e₂
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 : IsCoveringMapOn f Set.univ
Y : Type u_3
inst✝ : TopologicalSpace Y
g : X ≃ₜ Y
⊢ IsCoveringMapOn (⇑g ∘ f) Set.univ

Tactic:
exact hf.homeomorph_comp g

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

Goal state before:
pp: r s : ℝ
h : r ≤ s
⊢ centeredArc r ⊆ centeredArc s

Tactic:
by
  rintro _ ⟨x, hx, rfl⟩
  exact ⟨x, hx.trans_le h, rfl⟩

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

Goal state before:
pp: x y : Circle
hne : x ≠ y
⊢ (↑x).arg ≠ x.angleDiff y + (↑x).arg

Tactic:
simp [angleDiff_pos hne |>.ne']

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

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ (range ⇑(x.path y))ᶜ = ⇑(y.path x) '' Ioo 0 1

Tactic:
rw [range_path, ← Ioc_insert_left (by simp), image_insert_eq,
    ← path_image_Ioc_of_ne h, ← union_singleton, compl_union, compl_path_image_Ioc h,
    ← Ioo_insert_right (by simp), image_insert_eq, (y.path x).target, exp_arg,
    insert_inter_of_notMem (by simp), inter_eq_left]
  rintro z ⟨t, ht, rfl⟩
  exact (path_injective_of_ne h.symm).ne ht.2.ne |>.trans_eq (y.path x).target

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
⊢ argSelfAdjoint (expUnitary x) = x

Tactic:
nontriviality A
  ext
  have : spectrum ℂ (expUnitary x : A) ⊆ slitPlane := by
    rw [spectrum_subset_slitPlane_iff_norm_lt_two (expUnitary x).2,
      ← sq_lt_sq₀ (by positivity) (by positivity), norm_sq_expUnitary_sub_one hx.le]
    calc
      2 * (1 - Real.cos ‖x‖) < 2 * (1 - Real.cos π) := by
        gcongr
        exact Real.cos_lt_cos_of_nonneg_of_le_pi (by positivity) le_rfl hx
      _ = 2 ^ 2 := by norm_num
  simp only [argSelfAdjoint_coe, expUnitary_coe]
  rw [← CFC.exp_eq_normedSpace_exp (𝕜 := ℂ), ← cfc_comp_smul .., ← cfc_comp' (hg := ?hg)]
  case hg =>
    refine continuous_ofReal.comp_continuousOn <| continuousOn_arg.mono ?_
    rwa [expUnitary_coe, ← CFC.exp_eq_normedSpace_exp (𝕜 := ℂ), ← cfc_comp_smul ..,
      cfc_map_spectrum ..] at this
  conv_rhs => rw [← cfc_id' ℂ (x : A)]
  refine cfc_congr fun y hy ↦ ?_
  rw [← x.2.spectrumRestricts.algebraMap_image] at hy
  obtain ⟨y, hy, rfl⟩ := hy
  simp only [coe_algebraMap, smul_eq_mul, mul_comm I, ← exp_eq_exp_ℂ, ofReal_inj]
  replace hy : ‖y‖ < π := spectrum.norm_le_norm_of_mem hy |>.trans_lt hx
  simp only [Real.norm_eq_abs, abs_lt] at hy
  rw [← Circle.coe_exp, Circle.arg_exp hy.1 hy.2.le]

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✝ : CharZero k
s : Simplex k P n
t : Set (Fin (n + 1))
ht : t ≠ Set.univ
h : s.centroid ∈ affineSpan k (s.points '' t)
⊢ False

Tactic:
have hssubset : t ⊂ Set.univ := by grind

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✝ : CharZero k
s : Simplex k P n
t : Set (Fin (n + 1))
ht : t ≠ Set.univ
h : s.centroid ∈ affineSpan k (s.points '' t)
hssubset : t ⊂ Set.univ
⊢ False
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 : ℕ
s₁ s₂ : Simplex k P n
h : Set.range s₁.points = Set.range s₂.points
⊢ Finset.centroid k univ s₁.points = Finset.centroid k univ s₂.points

Tactic:
by
  rw [← Set.image_univ, ← Set.image_univ, ← Finset.coe_univ] at h
  exact
    Finset.univ.centroid_eq_of_inj_on_of_image_eq k _
      (fun _ _ _ _ he => AffineIndependent.injective s₁.independent he)
      (fun _ _ _ _ he => AffineIndependent.injective s₂.independent he) h

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
ι : Type u_5
b : Basis ι 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
⊢ A = adjoint B ↔ ∀ (i : ι) (x : E), ⟪A x, b i⟫_𝕜 = ⟪x, B (b i)⟫_𝕜

Tactic:
by
  refine ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => ?_⟩
  ext x
  exact ext_inner_right_basis b fun i => by simp only [h i, adjoint_inner_left]

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
hp₀v : ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀
w : V
hw : w ∈ vectorSpan k s
hs : vectorSpan k s ≤ k ∙ v
⊢ ∃ r, r • v = w

Tactic:
have hw' := SetLike.le_def.1 hs hw

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
hp₀v : ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀
w : V
hw : w ∈ vectorSpan k s
hs : vectorSpan k s ≤ k ∙ v
hw' : w ∈ k ∙ v
⊢ ∃ r, r • v = w
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

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

Tactic:
use 0
    simp [hp]

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

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
ι : Type u_3
inst✝ : Fintype ι
b : AffineBasis ι ℝ V
⊢ Finset.centroid ℝ Finset.univ ⇑b ∈ interior ((convexHull ℝ) (range ⇑b))

Tactic:
by
  have := b.nonempty
  simp only [b.interior_convexHull, mem_ofPred_eq, b.coord_apply_centroid (Finset.mem_univ _),
    inv_pos, Nat.cast_pos, Finset.card_pos, Finset.univ_nonempty, forall_true_iff]

Goal state after:
Module: Mathlib.Analysis.Calculus.BumpFunction.Basic

Goal state before:
pp: E : Type u_1
c : E
f : ContDiffBump c
⊢ 1 < f.rOut / f.rIn

Tactic:
rw [one_lt_div f.rIn_pos]

Goal state after:
E : Type u_1
c : E
f : ContDiffBump c
⊢ f.rIn < f.rOut
Module: Mathlib.MeasureTheory.Group.Integral

Goal state before:
pp: G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
μ : Measure G
f : G → E
g : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulLeftInvariant
hf' : ∀ (x : G), f (g * x) = -f x
this : IsAddTorsionFree E
⊢ ∫ (x : G), f x ∂μ = -∫ (x : G), f x ∂μ

Tactic:
← integral_neg,

Goal state after:
G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
μ : Measure G
f : G → E
g : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulLeftInvariant
hf' : ∀ (x : G), f (g * x) = -f x
this : IsAddTorsionFree E
⊢ ∫ (x : G), f x ∂μ = ∫ (a : G), -f a ∂μ