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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : a ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
x✝ : PartialOrder (Unitization ℂ A) := spectralOrder (Unitization ℂ A)
this✝ : StarOrderedRing (Unitization ℂ A)
this :
  (Unitization.inrNonUnitalStarAlgHom ℂ A) a ∈
    AddSubmonoid.closure (Set.range (⇑(Unitization.inrNonUnitalStarAlgHom ℂ A) ∘ fun s ↦ star s * s))
⊢ Set.range (⇑(Unitization.inrNonUnitalStarAlgHom ℂ A) ∘ fun s ↦ star s * s) ⊆ Set.range fun s ↦ star s * s

Tactic:
rintro _ ⟨s, rfl⟩

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : a ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s)
x✝ : PartialOrder (Unitization ℂ A) := spectralOrder (Unitization ℂ A)
this✝ : StarOrderedRing (Unitization ℂ A)
this :
  (Unitization.inrNonUnitalStarAlgHom ℂ A) a ∈
    AddSubmonoid.closure (Set.range (⇑(Unitization.inrNonUnitalStarAlgHom ℂ A) ∘ fun s ↦ star s * s))
s : A
⊢ (⇑(Unitization.inrNonUnitalStarAlgHom ℂ A) ∘ fun s ↦ star s * s) s ∈ Set.range fun s ↦ star s * s
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : ContinuousStar A
inst✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
hf : ContinuousOn f s
ha' : ∀ (x : X), p (a x)
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ cfc f (a x)

Tactic:
by
  rw [← continuousOn_univ] at ha_cont ⊢
  exact ha_cont.cfc' hs f (fun x _ ↦ ha x) (fun x _ ↦ ha' x)

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
⊢ ↑a ≤ ↑b⁻¹ ↔ ↑b ≤ ↑a⁻¹

Tactic:
by
  simpa using CStarAlgebra.inv_le_inv_iff (inv_nonneg_of_nonneg a ha) hb

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
ha : 0 ≤ a
hab : a ≤ b
this : ∀ (a b : Unitization ℂ A), 0 ≤ a → a ≤ b → ‖a‖ ≤ ‖b‖
hb : 0 ≤ b
⊢ ↑a ≤ ↑b

Tactic:
by rwa [Unitization.inr_le_iff a b]

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc f)
⊢ ConvexOn ℝ s (cfcₙ f)

Tactic:
let inrl : A →ₗ[ℝ] A⁺¹ := inrHom ℝ ℂ A

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ → ℝ
s : Set A
hf : ConvexOn ℝ (inr '' s) (cfc f)
inrl : A →ₗ[ℝ] Unitization ℂ A := inrHom ℝ ℂ A
⊢ ConvexOn ℝ s (cfcₙ f)
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✝
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
⊢ ‖sqrt a * (1 - e)‖ ^ 2 = 0

Tactic:
← norm_star_mul_mul_self_of_nonneg,

Goal state after:
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✝
a e : Unitization ℂ A
he : IsStarProjection e
ha : 0 ≤ a
hae : a ≤ e
⊢ ‖star (1 - e) * a * (1 - e)‖ = 0
Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions

Goal state before:
pp: A : Type u_1
inst✝⁹ : NonUnitalCStarAlgebra A
inst✝⁸ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : Module ℂ E
inst✝⁵ : SMul A E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : Module ℂ F
inst✝² : SMul A F
inst✝¹ : CStarModule A E
inst✝ : CStarModule A F
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ‖⟪x.1, x.1⟫_A‖ + ‖⟪x.2, x.2⟫_A‖ = ‖x.1‖ ^ 2 + 0 + ‖x.2‖ ^ 2

Tactic:
by simp [norm_sq_eq A]

Goal state after:
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:
nth_rw 1 [← one_mul z]
  rw [← sqrt_sq c, le_sqrt_iff_sq_le, ← sub_mul, sq, ← CStarRing.nnnorm_star_mul_self]
  simp only [star_mul, star_sub, star_one]
  have hy₀ : y ∈ Set.Icc 0 1 := ⟨hx₀.trans hy.1, hy.2⟩
  have hy' : 1 - y ∈ Set.Icc 0 1 := Set.sub_mem_Icc_zero_iff_right.mpr hy₀
  rw [hy₀.1.star_eq, ← mul_assoc, mul_assoc (star _), ← sq]
  refine nnnorm_le_nnnorm_of_nonneg_of_le (star_left_conjugate_nonneg (pow_nonneg hy'.1 2) _) ?_
    |>.trans h
  refine star_left_conjugate_le_conjugate ?_ _
  trans (1 - y)
  · simpa using pow_antitone hy'.1 hy'.2 one_le_two
  · gcongr
    exact hy.1

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✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ (Finset.univ.sup fun i ↦ ∑ j, ‖A i j‖₊ * ∑ k, ‖B j k‖₊) ≤
    Finset.univ.sup fun i ↦ ∑ j, ‖A i j‖₊ * Finset.univ.sup fun i ↦ ∑ j, ‖B i j‖₊

Tactic:
refine Finset.sup_mono_fun fun i _hi => ?_

Goal state after:
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✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
i : l
_hi : i ∈ Finset.univ
⊢ ∑ j, ‖A i j‖₊ * ∑ k, ‖B j k‖₊ ≤ ∑ j, ‖A i j‖₊ * Finset.univ.sup fun i ↦ ∑ j, ‖B i j‖₊
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: case frequently
X : Type u_1
𝕜 : 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
inst✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace ↑s
f : C(↑s, 𝕜)₀
hf :
  ∃ᶠ (g : C(↑s, 𝕜)₀) in 𝓝 f,
    Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcₙHomSuperset ⋯ ⋯) g
ε : ℝ
hε : 0 < ε
g : C(↑s, 𝕜)₀
g_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcₙHomSuperset ⋯ ⋯) g
hg : ‖f - g‖ ≤ ε
x : X
⊢ ‖(cfcₙHom ⋯) ((f - g).comp { toFun := Subtype.map id ⋯, continuous_toFun := ⋯, map_zero' := ⋯ })‖ ≤ ε

Tactic:
rw [isometry_cfcₙHom (R := 𝕜) _ (ha' x) |>.norm_map_of_map_zero (map_zero (cfcₙHom (ha' x)))]

Goal state after:
case frequently
X : Type u_1
𝕜 : 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
inst✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
hs0 : Fact (0 ∈ s)
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace ↑s
f : C(↑s, 𝕜)₀
hf :
  ∃ᶠ (g : C(↑s, 𝕜)₀) in 𝓝 f,
    Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcₙHomSuperset ⋯ ⋯) g
ε : ℝ
hε : 0 < ε
g : C(↑s, 𝕜)₀
g_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcₙHomSuperset ⋯ ⋯) g
hg : ‖f - g‖ ≤ ε
x : X
⊢ ‖(f - g).comp { toFun := Subtype.map id ⋯, continuous_toFun := ⋯, map_zero' := ⋯ }‖ ≤ ε
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute

Goal state before:
pp: A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module ℝ A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : IsTopologicalRing A
inst✝³ : T2Space A
inst✝² : PartialOrder A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : StarOrderedRing A
a b : A
hb : Commute a b
f : ℝ≥0 → ℝ≥0
⊢ Commute (cfcₙ f a) b

Tactic:
by_cases ha : 0 ≤ a
  · rw [cfcₙ_nnreal_eq_real ..]
    exact hb.cfcₙ_real _
  · simp [cfcₙ_apply_of_not_predicate a ha]

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

Goal state before:
pp: case inl
m : Type u_1
n : Type u_2
A : Type u_5
inst✝⁴ : Fintype m
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype n
M : CStarMatrix m n A
C : ℝ≥0
h : ∀ (v : C⋆ᵐᵒᵈ(A, m → A)) (w : C⋆ᵐᵒᵈ(A, n → A)), ‖⟪w, (toCLM M) v⟫_A‖ ≤ ↑C * ‖v‖ * ‖w‖
v : C⋆ᵐᵒᵈ(A, m → A)
h₀ : 0 = ‖(toCLM M) v‖
⊢ ‖(toCLM M) v‖ ≤ ↑C * ‖v‖

Tactic:
← h₀

Goal state after:
case inl
m : Type u_1
n : Type u_2
A : Type u_5
inst✝⁴ : Fintype m
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype n
M : CStarMatrix m n A
C : ℝ≥0
h : ∀ (v : C⋆ᵐᵒᵈ(A, m → A)) (w : C⋆ᵐᵒᵈ(A, n → A)), ‖⟪w, (toCLM M) v⟫_A‖ ≤ ↑C * ‖v‖ * ‖w‖
v : C⋆ᵐᵒᵈ(A, m → A)
h₀ : 0 = ‖(toCLM M) v‖
⊢ 0 ≤ ↑C * ‖v‖
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart

Goal state before:
pp: A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : Module ℂ A
inst✝³ : IsScalarTower ℂ A A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : StarModule ℂ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
⊢ quasispectrum ℂ ↑(ℜ a) = (fun x ↦ ↑x.re) '' quasispectrum ℂ a

Tactic:
← cfcₙ_re_id a,

Goal state after:
A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : Module ℂ A
inst✝³ : IsScalarTower ℂ A A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : StarModule ℂ A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
a : A
ha : IsStarNormal a
⊢ quasispectrum ℂ (cfcₙ (fun x ↦ ↑x.re) a) = (fun x ↦ ↑x.re) '' quasispectrum ℂ a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart

Goal state before:
pp: A : Type u_1
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℂ A
inst✝⁴ : IsScalarTower ℂ A A
inst✝³ : SMulCommClass ℂ A A
inst✝² : StarModule ℂ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝ : ContinuousMapZero.UniqueHom ℂ A
f : ℂ → ℂ
a : A
hf : ContinuousOn f ((fun x ↦ ↑x.re) '' quasispectrum ℂ a)
hf0 : f 0 = 0
ha : IsStarNormal a
⊢ cfcₙ f ↑(ℜ a) = cfcₙ (fun x ↦ f ↑x.re) a

Tactic:
← cfcₙ_re_id a,

Goal state after:
A : Type u_1
inst✝⁸ : TopologicalSpace A
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℂ A
inst✝⁴ : IsScalarTower ℂ A A
inst✝³ : SMulCommClass ℂ A A
inst✝² : StarModule ℂ A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝ : ContinuousMapZero.UniqueHom ℂ A
f : ℂ → ℂ
a : A
hf : ContinuousOn f ((fun x ↦ ↑x.re) '' quasispectrum ℂ a)
hf0 : f 0 = 0
ha : IsStarNormal a
⊢ cfcₙ f (cfcₙ (fun x ↦ ↑x.re) a) = cfcₙ (fun x ↦ f ↑x.re) a
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart

Goal state before:
pp: A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module ℂ A
inst✝⁵ : IsScalarTower ℂ A A
inst✝⁴ : SMulCommClass ℂ A A
inst✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMapZero.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (quasispectrum ℝ ↑(ℜ a))
hf0 : f 0 = 0
ha : IsStarNormal a
this : ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.re) '' quasispectrum ℂ a)
| cfcₙ (fun x ↦ ↑(f x.re)) ↑(ℜ a)

Tactic:
← cfcₙ_re_id a,

Goal state after:
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module ℂ A
inst✝⁵ : IsScalarTower ℂ A A
inst✝⁴ : SMulCommClass ℂ A A
inst✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMapZero.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (quasispectrum ℝ ↑(ℜ a))
hf0 : f 0 = 0
ha : IsStarNormal a
this : ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.re) '' quasispectrum ℂ a)
| cfcₙ (fun x ↦ ↑(f x.re)) (cfcₙ (fun x ↦ ↑x.re) a)
Module: Mathlib.Analysis.InnerProductSpace.Dual

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ).ker
htriv : Y = ⊤
hℓ : ℓ = 0
⊢ ∃ a, (toDualMap 𝕜 E) a = ℓ

Tactic:
exact ⟨0, by simp [hℓ]⟩

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

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ).ker
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
apply ContinuousLinearMap.ext

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := ⋯
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e e' : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
⊢ (e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf) = e.symm.trans e'

Tactic:
by
  ext z
  · exact e.lift_openEmbedding_trans_apply e' hf z
  · simp [hf.injective.extend_apply e]
  · simp_rw [OpenPartialHomeomorph.trans_source, e.lift_openEmbedding_symm_source, e.symm_source,
      e.lift_openEmbedding_symm, e'.lift_openEmbedding_source]
    refine ⟨fun ⟨hx, ⟨y, hy, hxy⟩⟩ ↦ ⟨hx, ?_⟩, fun ⟨hx, hx'⟩ ↦ ⟨hx, mem_image_of_mem f hx'⟩⟩
    rw [mem_preimage]; rw [comp_apply] at hxy
    exact (hf.injective hxy) ▸ hy

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 : ι
t : Set Z.TotalSpace
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ ↑(Z.localTrivAsPartialEquiv j) ⁻¹' s
e : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv i
⊢ IsOpen[instTopologicalSpaceProd]
    ((Z.localTrivAsPartialEquiv i).target ∩
      ((Z.localTrivAsPartialEquiv i).invFun ⁻¹' (Z.localTrivAsPartialEquiv j).source ∩
        (Z.localTrivAsPartialEquiv i).invFun ⁻¹' ↑(Z.localTrivAsPartialEquiv j) ⁻¹' s))

Tactic:
let e' := Z.localTrivAsPartialEquiv j

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
i : ι
t : Set Z.TotalSpace
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ ↑(Z.localTrivAsPartialEquiv j) ⁻¹' s
e : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv i
e' : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv j
⊢ IsOpen[instTopologicalSpaceProd]
    ((Z.localTrivAsPartialEquiv i).target ∩
      ((Z.localTrivAsPartialEquiv i).invFun ⁻¹' (Z.localTrivAsPartialEquiv j).source ∩
        (Z.localTrivAsPartialEquiv i).invFun ⁻¹' ↑(Z.localTrivAsPartialEquiv j) ⁻¹' s))
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 : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ ↑e.symm) (↑e z)
hez : z ∈ e.symm.target
⊢ ContinuousAt f z

Tactic:
rwa [e.toOpenPartialHomeomorph.symm.continuousAt_iff_continuousAt_comp_right hez,
    OpenPartialHomeomorph.symm_symm]

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
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x✝ : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
inst✝¹ : LinearOrder B
inst✝ : OrderTopology B
e e' : Trivialization F proj
a : B
He : a ∈ e.baseSet
He' : a ∈ e'.baseSet
Heq : ∀ (p : Z), proj p = a → ↑e p = ↑e' p
x : B
hx : x ∈ frontier (Iic a)
⊢ x ∈ e.baseSet ↔ x ∈ e'.baseSet

Tactic:
obtain rfl : x = a := mem_singleton_iff.1 (frontier_Iic_subset _ hx)

Goal state after:
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
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x✝ : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
inst✝¹ : LinearOrder B
inst✝ : OrderTopology B
e e' : Trivialization F proj
x : B
He : x ∈ e.baseSet
He' : x ∈ e'.baseSet
Heq : ∀ (p : Z), proj p = x → ↑e p = ↑e' p
hx : x ∈ frontier (Iic x)
⊢ x ∈ e.baseSet ↔ x ∈ e'.baseSet
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
inst✝ : DiscreteTopology I
x : X
t : Trivialization I f
hx : x ∈ t.baseSet
xi : ↑t.baseSet × I
⊢ t.invFun (↑xi.1, xi.2) ∈ f ⁻¹' t.baseSet

Tactic:
rw [Set.mem_preimage, ← t.mem_source]; exact t.map_target (t.target_eq ▸ ⟨xi.1.2, ⟨⟩⟩)

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

Goal state before:
pp: r : ℝ
hr : r ≤ π
z : Circle
⊢ z ∈ centeredArc r ↔ |(↑z).arg| < r

Tactic:
refine ⟨?_, fun hz ↦ ⟨arg z, hz, exp_arg z⟩⟩

Goal state after:
r : ℝ
hr : r ≤ π
z : Circle
⊢ z ∈ centeredArc r → |(↑z).arg| < r
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: case h
A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
⊢ Real.cos π < Real.cos ‖x‖

Tactic:
exact Real.cos_lt_cos_of_nonneg_of_le_pi (by positivity) le_rfl hx

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
A : E →ₗ[𝕜] F
⊢ finrank 𝕜 ↥(adjoint A).range = finrank 𝕜 F - finrank 𝕜 ↥(adjoint A).ker

Tactic:
simp [← A.adjoint.finrank_range_add_finrank_ker]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: case mpr
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
p : P
this : ∑ i, (s.points i -ᵥ p) = ∑ i, (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid))
h : (n + 1) • (p -ᵥ s.centroid) = 0
h' : (↑n + 1) • (p -ᵥ s.centroid) = 0
⊢ p -ᵥ s.centroid = 0

Tactic:
smul_eq_zero_iff_right (by norm_cast)

Goal state after:
case mpr
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
p : P
this : ∑ i, (s.points i -ᵥ p) = ∑ i, (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid))
h : (n + 1) • (p -ᵥ s.centroid) = 0
h' : p -ᵥ s.centroid = 0
⊢ p -ᵥ s.centroid = 0
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
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
hc' : #(Finset.image p s) = n + 1
p₁ : P
hi' : LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' (↑(Finset.image p s) \ ↑{p₁}))) ↦ ↑v
hp₁ : p₁ ∈ Finset.image p s
hp₁' : p₁ ∈ p '' ↑s
⊢ finrank k ↥(vectorSpan k ↑(Finset.image p s)) = n

Tactic:
← Finset.coe_sdiff,

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
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
hc' : #(Finset.image p s) = n + 1
p₁ : P
hi' : LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' ↑(Finset.image p s \ {p₁}))) ↦ ↑v
hp₁ : p₁ ∈ Finset.image p s
hp₁' : p₁ ∈ p '' ↑s
⊢ finrank k ↥(vectorSpan k ↑(Finset.image p s)) = n
Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases

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

Tactic:
cases subsingleton_or_nontrivial ι
  · -- The zero-dimensional case.
    have : range b = univ :=
      AffineSubspace.eq_univ_of_subsingleton_span_eq_top (subsingleton_range _) b.tot
    simp [this]
  · -- The positive-dimensional case.
    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.Calculus.BumpFunction.Basic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
f : ContDiffBump 0
x : E
⊢ ↑f (0 + x) = ↑f x

Tactic:
zero_add

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

Goal state before:
pp: case neg
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 : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k ↥s.direction
hf' : ¬FiniteDimensional k ↥(vectorSpan k (insert p ↑s))
⊢ 0 ≤ 0 + 1

Tactic:
zero_add

Goal state after:
case neg
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 : AffineSubspace k P
p : P
hf : ¬FiniteDimensional k ↥s.direction
hf' : ¬FiniteDimensional k ↥(vectorSpan k (insert p ↑s))
⊢ 0 ≤ 1
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case pos.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
s : AffineSubspace k P
p : P
hf : FiniteDimensional k ↥s.direction
hs : s = ⊥
⊢ finrank k ↥(vectorSpan k (insert p ∅)) ≤ 0 + 1

Tactic:
zero_add

Goal state after:
case pos.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
s : AffineSubspace k P
p : P
hf : FiniteDimensional k ↥s.direction
hs : s = ⊥
⊢ finrank k ↥(vectorSpan k (insert p ∅)) ≤ 1