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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
b : A
⊢ ∀ x ∈ spectrum ℝ (star b * b), 0 ≤ x

Tactic:
set a := star b * b with a_def
  have ha : IsSelfAdjoint a := by simp [a_def]
  -- the key element to consider is `c := b * a⁻`, which satisfies `- (star c * c) = a⁻ ^ 3`.
  set c := b * a⁻
  have h_eq_negPart_a : -(star c * c) = a⁻ ^ 3 := calc
    -(star c * c) = - a⁻ * a * a⁻ := by
      simp only [star_mul, c, mul_assoc, ← mul_assoc (star b), ← a_def, CFC.negPart_def,
        neg_mul, IsSelfAdjoint.cfcₙ (f := (·⁻)).star_eq]
    _ = - a⁻ * (a⁺ - a⁻) * a⁻ :=
      congr(- a⁻ * $(CFC.posPart_sub_negPart a ha) * a⁻).symm
    _ = a⁻ ^ 3 := by simp [mul_sub, pow_succ]
  -- the spectrum of `- (star c * c) = a⁻ ^ 3` is nonnegative, since the function on the right
  -- is nonnegative on the spectrum of `a`.
  have h_c_spec₀ : SpectrumRestricts (-(star c * c)) (ContinuousMap.realToNNReal ·) := by
    simp only [SpectrumRestricts.nnreal_iff, h_eq_negPart_a, CFC.negPart_def]
    rw [cfcₙ_eq_cfc (hf0 := by simp), ← cfc_pow (ha := ha) .., cfc_map_spectrum (ha := ha) ..]
    rintro - ⟨x, -, rfl⟩
    positivity
  -- the spectrum of `c * star c` is nonnegative, since squares of selfadjoint elements have
  -- nonnegative spectrum, and `c * star c = 2 • (ℜ c ^ 2 + ℑ c ^ 2) + (- (star c * c))`,
  -- and selfadjoint elements with nonnegative spectrum are closed under addition.
  have h_c_spec₁ : SpectrumRestricts (c * star c) ContinuousMap.realToNNReal := by
    rw [eq_sub_iff_add_eq'.mpr <| star_mul_self_add_self_mul_star c, sub_eq_add_neg, ← sq, ← sq]
    refine SpectrumRestricts.nnreal_add ?_ ?_ ?_ h_c_spec₀
    · exact .smul (star_trivial _) <| ((ℜ c).prop.pow 2).add ((ℑ c).prop.pow 2)
    · exact .neg <| .star_mul_self c
    · rw [← Nat.cast_smul_eq_nsmul ℝ]
      refine (ℜ c).2.sq_spectrumRestricts.nnreal_add ((ℜ c).2.pow 2) ((ℑ c).2.pow 2)
        (ℑ c).2.sq_spectrumRestricts |>.smul_of_nonneg <| by simp
  -- therefore `- (star c * c) = 0` and so `a⁻ ^ 3 = 0`. By properties of the continuous functional
  -- calculus, `fun x ↦ x⁻ ^ 3` is zero on the spectrum of `a`, `0 ≤ x` for `x ∈ spectrum ℝ a`.
  rw [h_c_spec₁.mul_comm.eq_zero_of_neg (.star_mul_self c) h_c_spec₀, neg_zero, CFC.negPart_def,
    cfcₙ_eq_cfc (hf0 := by simp), ← cfc_pow _ _ (ha := ha), ← cfc_zero a (R := ℝ)] at h_eq_negPart_a
  have h_eqOn := eqOn_of_cfc_eq_cfc (ha := ha) h_eq_negPart_a
  exact fun x hx ↦ negPart_eq_zero.mp <| eq_zero_of_pow_eq_zero (h_eqOn hx).symm

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
B : Type u_2
inst✝¹² : PartialOrder B
inst✝¹¹ : Ring B
inst✝¹⁰ : StarRing B
inst✝⁹ : TopologicalSpace B
inst✝⁸ : StarOrderedRing B
inst✝⁷ : Algebra ℝ B
inst✝⁶ : ContinuousFunctionalCalculus ℝ B IsSelfAdjoint
inst✝⁵ : ContinuousFunctionalCalculus ℝ (A × B) IsSelfAdjoint
inst✝⁴ : IsSemitopologicalRing B
inst✝³ : T2Space B
inst✝² : StarOrderedRing (A × B)
inst✝¹ : NonnegSpectrumClass ℝ B
inst✝ : NonnegSpectrumClass ℝ (A × B)
a : A
b : B
x : ℝ
ha : IsUnit a
hb : IsUnit b
ha' : 0 ≤ a
hb' : 0 ≤ b
⊢ rpow (a, b) x = (a ^ x, b ^ x)

Tactic:
by
  have ha'' : 0 ∉ spectrum ℝ≥0 a := spectrum.zero_notMem _ ha
  have hb'' : 0 ∉ spectrum ℝ≥0 b := spectrum.zero_notMem _ hb
  simp only [rpow_def]
  unfold rpow
  refine cfc_map_prod (R := ℝ≥0) (S := ℝ) _ a b (by cfc_cont_tac) ?_
  rw [Prod.le_def]
  constructor <;> simp [ha', hb']

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
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
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ‖x‖ ≤ ↑2 * ‖(linearEquiv ℂ A (E × F)) x‖

Tactic:
apply prod_norm_le_norm_add x |>.trans

Goal state after:
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
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ‖x.1‖ + ‖x.2‖ ≤ ↑2 * ‖(linearEquiv ℂ A (E × F)) x‖
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
A : Type u_2
inst✝¹¹ : NormedRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : NormedAlgebra ℝ A
inst✝⁸ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁷ : ContinuousStar A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : NonnegSpectrumClass ℝ A
inst✝³ : T2Space A
inst✝² : IsSemitopologicalRing A
inst✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
hs : s ∈ 𝓝ˢ (⋃ x, spectrum ℝ≥0 (a x))
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha' : ∀ (x : X), 0 ≤ a x
hf : ContinuousOn f s
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ cfc f (a x)

Tactic:
by
  rw [← continuousOn_univ] at ha_cont ⊢
  exact ha_cont.cfc_nnreal_of_mem_nhdsSet f (by simpa) (by simpa)

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hxy : x ≤ y
hy₁ : ‖y‖ ≤ 1
c : ℝ
hc : 0 ≤ c
h : ‖star ↑z * (1 - ↑x) * ↑z‖ ≤ c ^ 2
⊢ ‖↑(z - y * z)‖ ≤ c

Tactic:
inr_sub,

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hxy : x ≤ y
hy₁ : ‖y‖ ≤ 1
c : ℝ
hc : 0 ≤ c
h : ‖star ↑z * (1 - ↑x) * ↑z‖ ≤ c ^ 2
⊢ ‖↑z - ↑(y * z)‖ ≤ c
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝ m : A
hm₁ : 0 ≤ ↑m
hm₂ : ‖↑m‖ < 1
ε : ℝ≥0
hε : 0 < ε
x : A
hx₁ : cfc (fun y ↦ 1 - (1 + y)⁻¹) (ε⁻¹ ^ 2 • ↑m) ≤ ↑x
hx₂ : ‖↑x‖ ≤ 1
hx₀ : 0 ≤ ↑x
⊢ ‖↑(m - x * m)‖₊ ≤ ε

Tactic:
inr_sub,

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝ m : A
hm₁ : 0 ≤ ↑m
hm₂ : ‖↑m‖ < 1
ε : ℝ≥0
hε : 0 < ε
x : A
hx₁ : cfc (fun y ↦ 1 - (1 + y)⁻¹) (ε⁻¹ ^ 2 • ↑m) ≤ ↑x
hx₂ : ‖↑x‖ ≤ 1
hx₀ : 0 ≤ ↑x
⊢ ‖↑m - ↑(x * m)‖₊ ≤ ε
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✝⁷ : 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)
f : C(↑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
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (cfcₙHomSuperset ⋯ ⋯) f

Tactic:
induction f using ContinuousMapZero.induction_on_of_compact with
  | zero => simpa [map_zero] using! continuous_const
  | id => simpa only [cfcₙHomSuperset_id]
  | star_id => simp only [map_star, cfcₙHomSuperset_id]; fun_prop
  | add f g hf hg => simpa only [map_add] using! hf.add hg
  | mul f g hf hg => simpa only [map_mul] using! hf.mul hg
  | smul r f hf => simpa only [map_smul] using! hf.const_smul r
  | frequently f hf =>
    apply continuous_of_uniform_approx_of_continuous
    rw [Metric.uniformity_basis_dist_le.forall_iff (by aesop)]
    intro ε hε
    simp only [Set.mem_ofPred_eq, dist_eq_norm]
    obtain ⟨g, hg, g_cont⟩ := frequently_iff.mp hf (Metric.closedBall_mem_nhds f hε)
    simp only [Metric.mem_closedBall, dist_comm g, dist_eq_norm] at hg
    refine ⟨_, g_cont, fun x ↦ ?_⟩
    rw [← map_sub, cfcₙHomSuperset_apply]
    rw [isometry_cfcₙHom (R := 𝕜) _ (ha' x) |>.norm_map_of_map_zero (map_zero (cfcₙHom (ha' x)))]
    rw [ContinuousMapZero.norm_def, ContinuousMap.norm_le _ hε.le] at hg ⊢
    aesop

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

Goal state before:
pp: case frequently
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra 𝕜 A
inst✝³ : TopologicalSpace A
inst✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f : C(↑(spectrum 𝕜 a), 𝕜)
hf : ∃ᶠ (g : C(↑(spectrum 𝕜 a), 𝕜)) in nhds f, Commute ((cfcHom ha) g) b
⊢ (cfcHom ha) f ∈ closure {y | y * b = b * y}

Tactic:
apply mem_closure_of_frequently_of_tendsto hf

Goal state after:
case frequently
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra 𝕜 A
inst✝³ : TopologicalSpace A
inst✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f : C(↑(spectrum 𝕜 a), 𝕜)
hf : ∃ᶠ (g : C(↑(spectrum 𝕜 a), 𝕜)) in nhds f, Commute ((cfcHom ha) g) b
⊢ Filter.Tendsto (⇑(cfcHom ha)) (nhds f) (nhds ((cfcHom ha) f))
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute

Goal state before:
pp: case frequently
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f : C(↑(quasispectrum 𝕜 a), 𝕜)₀
hf : ∃ᶠ (g : C(↑(quasispectrum 𝕜 a), 𝕜)₀) in nhds f, Commute ((cfcₙHom ha) g) b
⊢ (cfcₙHom ha) f ∈ closure {y | y * b = b * y}

Tactic:
apply mem_closure_of_frequently_of_tendsto hf

Goal state after:
case frequently
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : Module 𝕜 A
inst✝⁵ : IsScalarTower 𝕜 A A
inst✝⁴ : SMulCommClass 𝕜 A A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a b : A
ha : p a
hb₁ : Commute a b
hb₂ : Commute (star a) b
f : C(↑(quasispectrum 𝕜 a), 𝕜)₀
hf : ∃ᶠ (g : C(↑(quasispectrum 𝕜 a), 𝕜)₀) in nhds f, Commute ((cfcₙHom ha) g) b
⊢ Filter.Tendsto (⇑(cfcₙHom ha)) (nhds f) (nhds ((cfcₙHom ha) f))
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
R : Type ?u.14
A : Type ?u.16
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid A
inst✝² : Mul A
inst✝¹ : Module R A
inst✝ : Star A
e : m ≃ n
M : CStarMatrix m m A
i✝ j✝ : n
⊢ star (M (e.symm j✝) (e.symm i✝)) = star (Matrix.submatrix M ⇑e.symm ⇑e.symm) i✝ j✝

Tactic:
star_apply

Goal state after:
m : Type u_1
n : Type u_2
R✝ : Type u_3
S : Type u_4
A✝ : Type u_5
B : Type u_6
R : Type ?u.14
A : Type ?u.16
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid A
inst✝² : Mul A
inst✝¹ : Module R A
inst✝ : Star A
e : m ≃ n
M : CStarMatrix m m A
i✝ j✝ : n
⊢ star (M (e.symm j✝) (e.symm i✝)) = star (Matrix.submatrix M (⇑e.symm) (⇑e.symm) j✝ i✝)
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: A : Type u_1
inst✝⁴ : CStarAlgebra A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
r : ℂ
M : CStarMatrix n n A
⊢ ‖r • M‖ ≤ ‖r‖ * ‖M‖

Tactic:
simpa only [norm_def, map_smul] using (toCLM M).opNorm_smul_le r

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ Continuous (uncurry (inner 𝕜))

Tactic:
by
  let inner' : E →+ E →+ 𝕜 :=
    { toFun := fun x => (innerₛₗ 𝕜 x).toAddMonoidHom
      map_zero' := by ext x; exact inner_zero_left _
      map_add' := fun x y => by ext z; exact inner_add_left _ _ _ }
  have : Continuous fun p : E × E => inner' p.1 p.2 := continuous_inner
  rw [Completion.toInner, inner, uncurry_curry _]
  change
    Continuous
      (((isDenseInducing_toCompl E).prodMap (isDenseInducing_toCompl E)).extend fun p : E × E =>
        inner' p.1 p.2)
  exact (isDenseInducing_toCompl E).extend_Z_bilin (isDenseInducing_toCompl E) this

Goal state after:
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₂
inst✝¹ : T0Space β
inst✝ : CompleteSpace β
f : α →SL[σ] β
c : R₁
a : Completion α
⊢ ∀ (a : α), (↑((↑f).toAddMonoidHom.extension ⋯)).toFun (c • ↑a) = σ c • (↑((↑f).toAddMonoidHom.extension ⋯)).toFun ↑a

Tactic:
simp [← Completion.coe_smul, AddMonoidHom.extension_coe f.toAddMonoidHom f.continuous]

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
m : ℂ
x : A
⊢ (f.leftMulMapPreGNS (m • x)).completion = m • (f.leftMulMapPreGNS x).completion

Tactic:
by
  ext a
  induction a using induction_on with
  | hp =>
    exact isClosed_eq (f.leftMulMapPreGNS (m • x)).completion.continuous
      (m • (f.leftMulMapPreGNS x).completion).continuous
  | ih a => simp [smul_mul_assoc]

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

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

Tactic:
by grw [sub_nonneg, this, one_le_two]

Goal state after:
Module: Mathlib.Data.Bundle

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
⊢ range (mk b) = proj ⁻¹' {b}

Tactic:
by
  apply Subset.antisymm
  · rintro _ ⟨x, rfl⟩
    rfl
  · rintro ⟨_, x⟩ rfl
    exact ⟨x, rfl⟩

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

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 : OpenPartialHomeomorph X Y
e' : OpenPartialHomeomorph Y Z
f'' : Z ≃ₜ Z'
⊢ (e.trans e').transHomeomorph f'' = e.trans (e'.transHomeomorph f'')

Tactic:
simp only [transHomeomorph_eq_trans, trans_assoc]

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
hyV : ↑e.symm y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
⊢ ↑(V.openPartialHomeomorphSubtypeCoe hV).symm (↑e.symm y) =
    i (↑(U.openPartialHomeomorphSubtypeCoe hU).symm (↑e.symm y))

Tactic:
refine (V.openPartialHomeomorphSubtypeCoe hV).injOn ?_ trivial ?_

Goal state after:
case refine_1
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
hyV : ↑e.symm y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
⊢ ↑(V.openPartialHomeomorphSubtypeCoe hV).symm (↑e.symm y) ∈ (V.openPartialHomeomorphSubtypeCoe hV).source

case refine_2
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
hyV : ↑e.symm y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target
⊢ ↑(V.openPartialHomeomorphSubtypeCoe hV) (↑(V.openPartialHomeomorphSubtypeCoe hV).symm (↑e.symm y)) =
    ↑(V.openPartialHomeomorphSubtypeCoe hV) (i (↑(U.openPartialHomeomorphSubtypeCoe hU).symm (↑e.symm y)))
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
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc✝ : c ∈ Icc a b
hlt : a < c
ec : Trivialization F TotalSpace.proj
hc : c ∈ ec.baseSet
c' : B
hc' : c' ∈ Ico a c
hc'e : Ioc c' c ⊆ ec.baseSet
d : B
hd : d ∈ Ioc c' c
hdab : d ∈ Icc a b
ead : Trivialization F TotalSpace.proj
had : Icc a d ⊆ ead.baseSet
⊢ ∃ e, Icc a c ⊆ e.baseSet

Tactic:
refine ⟨ead.piecewiseLe ec d (had ⟨hdab.1, le_rfl⟩) (hc'e hd), subset_ite.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
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc✝ : c ∈ Icc a b
hlt : a < c
ec : Trivialization F TotalSpace.proj
hc : c ∈ ec.baseSet
c' : B
hc' : c' ∈ Ico a c
hc'e : Ioc c' c ⊆ ec.baseSet
d : B
hd : d ∈ Ioc c' c
hdab : d ∈ Icc a b
ead : Trivialization F TotalSpace.proj
had : Icc a d ⊆ ead.baseSet
⊢ Icc a c ∩ Iic d ⊆ ead.baseSet ∧ Icc a c \ Iic d ⊆ (ec.transFiberHomeomorph (ec.coordChangeHomeomorph ead ⋯ ⋯)).baseSet
Module: Mathlib.Topology.FiberBundle.Basic

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

Tactic:
rcases he with ⟨d', hdd' : d' < d, hd'c⟩

Goal state after:
case neg
B : Type u_2
F : Type u_3
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace F
E : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (b : B) → TopologicalSpace (E b)
inst✝² : ConditionallyCompleteLinearOrder B
inst✝¹ : OrderTopology B
inst✝ : FiberBundle F E
a b : B
ea : Trivialization F TotalSpace.proj
hea : a ∈ ea.baseSet
hab : a ≤ b
s : Set B := {x | x ∈ Icc a b ∧ ∃ e, Icc a x ⊆ e.baseSet}
ha : a ∈ s
sne : s.Nonempty
hsb : b ∈ upperBounds s
sbd : BddAbove s
c : B := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
ec : Trivialization F TotalSpace.proj
hec : Icc a c ⊆ ec.baseSet
hlt : c < b
d : B
hdcb : d ∈ Ioc c b
hd : Ico c d ⊆ ec.baseSet
had : Ico a d ⊆ ec.baseSet
d' : B
hdd' : d' < d
hd'c : d' ∈ Ioi c
⊢ ∃ d ∈ Ioc c b, ∃ e, Icc a d ⊆ e.baseSet
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 : ι
⊢ ∀ ⦃x : Z.TotalSpace⦄,
    x ∈ Z.proj ⁻¹' Z.baseSet i →
      { proj := (x.proj, Z.coordChange (Z.indexAt x.proj) i x.proj x.snd).1,
          snd :=
            Z.coordChange i (Z.indexAt (x.proj, Z.coordChange (Z.indexAt x.proj) i x.proj x.snd).1)
              (x.proj, Z.coordChange (Z.indexAt x.proj) i x.proj x.snd).1
              (x.proj, Z.coordChange (Z.indexAt x.proj) i x.proj x.snd).2 } =
        x

Tactic:
by
    rintro ⟨x, v⟩ hx
    replace hx : x ∈ Z.baseSet i := hx
    dsimp only
    rw [Z.coordChange_comp, Z.coordChange_self] <;> apply_rules [mem_baseSet_at, mem_inter]

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
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, ⋯⟩}
⊢ IsOpen[instTopologicalSpaceSubtype] {x}

Tactic:
refine ⟨e.source ∩ e ⁻¹' U, e.continuousOn_toFun.isOpen_inter_preimage e.open_source hU,
      subset_antisymm (fun x' mem ↦ Subtype.ext <| e.injOn mem.1 hx ?_) ?_⟩

Goal state after:
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

case refine_2
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} ⊆ Subtype.val ⁻¹' (e.source ∩ ↑e ⁻¹' U)
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: case inl
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
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp : p ∈ e.source
⊢ (↑(e.disjointUnion e'.toOpenPartialHomeomorph ⋯ ⋯) p).1 = proj p

Tactic:
change (e.source.piecewise e e' p).1 = proj p

Goal state after:
case inl
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
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
p : Z
hp : p ∈ e.source
⊢ (e.source.piecewise (↑e) (↑e') p).1 = proj p