mathlib-initiative/mathlib-tactics huggingface dataset:
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
hx : 0 < x
⊢ cfcₙ (fun x_1 ↦ x_1.nnrpow x) a = cfc (fun x_1 ↦ x_1 ^ ↑x) a

Tactic:
cfcₙ_eq_cfc

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
hx : 0 < x
⊢ cfc (fun x_1 ↦ x_1.nnrpow x) a = cfc (fun x_1 ↦ x_1 ^ ↑x) a
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
⊢ cfcₙ (⇑NNReal.sqrt) a = cfc (⇑NNReal.sqrt) a

Tactic:
cfcₙ_eq_cfc

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
⊢ cfc (⇑NNReal.sqrt) a = cfc (⇑NNReal.sqrt) a
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
htriv : ¬0 ≤ a
⊢ sqrt (a ^ ↑x) = a ^ (↑x / 2)

Tactic:
simp [sqrt_eq_cfc, rpow_def, cfc_apply_of_not_predicate a htriv]

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
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ cfc (fun x ↦ 1 - (1 + x)⁻¹) ↑a ≤ cfc (fun x ↦ 1 - (1 + x)⁻¹) ↑b

Tactic:
← inr_le_iff a b (.of_nonneg ha) (.of_nonneg hb)

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : ↑a ≤ ↑b
ha : 0 ≤ a
hb : 0 ≤ b
⊢ cfc (fun x ↦ 1 - (1 + x)⁻¹) ↑a ≤ cfc (fun x ↦ 1 - (1 + x)⁻¹) ↑b
Module: Mathlib.Analysis.CStarAlgebra.Module.Constructions

Goal state before:
pp: A : Type u_1
inst✝⁸ : NonUnitalCStarAlgebra A
inst✝⁷ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁶ : Fintype ι
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → Module ℂ (E i)
inst✝³ : (i : ι) → SMul A (E i)
inst✝² : (i : ι) → CStarModule A (E i)
inst✝¹ : StarOrderedRing A
inst✝ : DecidableEq ι
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
y : E i
⊢ ⟪(equiv A ((j : ι) → E j)).symm (Pi.single i y), x⟫_A = ⟪y, x i⟫_A

Tactic:
by
  simp only [pi_inner, equiv_symm_pi_apply]
  rw [Finset.sum_eq_single i]
  all_goals simp_all

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

Goal state before:
pp: A : Type u_1
inst✝⁸ : NonUnitalCStarAlgebra A
inst✝⁷ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁶ : Fintype ι
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → Module ℂ (E i)
inst✝³ : (i : ι) → SMul A (E i)
inst✝² : (i : ι) → CStarModule A (E i)
inst✝¹ : StarOrderedRing A
inst✝ : DecidableEq ι
x : C⋆ᵐᵒᵈ(A, (i : ι) → E i)
i : ι
y : E i
⊢ ⟪x, (equiv A ((i : ι) → E i)).symm (Pi.single i y)⟫_A = ⟪x i, y⟫_A

Tactic:
by
  simp only [pi_inner, equiv_symm_pi_apply]
  rw [Finset.sum_eq_single i]
  all_goals simp_all

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
f : ℝ≥0 → ℝ≥0 := fun x ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x ↦ x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
| a

Tactic:
rw [← cfcₙ_id ℝ≥0 a]

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : ℝ≥0 → ℝ≥0 := fun x ↦ 1 - (1 + x)⁻¹
g : ℝ≥0 → ℝ≥0 := fun x ↦ x * (1 - x)⁻¹
a b : A
ha₁ : 0 ≤ a
ha₂ : ‖a‖ < 1
| cfcₙ id a
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun x ↦ x * m) l (𝓝 m)
m : A
⊢ m ∈ span ℂ ({x | 0 ≤ x} ∩ ball 0 1)

Tactic:
simp [span_nonneg_inter_unitBall]

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'
    filter_upwards [hl] with x hx
    simp [hx.star_eq]

Goal state after:
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'
    filter_upwards [hl] with x hx
    simp [hx.star_eq]

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

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
hN : ∀ (x : n → α), ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x‖₊ ≤ N * ‖x‖₊
⊢ (Finset.univ.sup fun i ↦ ∑ j, ‖A i j‖₊) ≤ N

Tactic:
refine Finset.sup_le fun i _ => ?_

Goal state after:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
hN : ∀ (x : n → α), ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x‖₊ ≤ N * ‖x‖₊
i : m
x✝ : i ∈ Finset.univ
⊢ ∑ j, ‖A i j‖₊ ≤ N
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
hN : ∀ (x : n → α), ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x‖₊ ≤ N * ‖x‖₊
i : m
x✝ : i ∈ Finset.univ
h✝ : Nonempty n
x : n → α := fun j ↦ unitOf (A i j)
⊢ ‖x‖₊ = 1

Tactic:
x,

Goal state after:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
hN : ∀ (x : n → α), ‖{ toLinearMap := A.mulVecLin, cont := ⋯ } x‖₊ ≤ N * ‖x‖₊
i : m
x✝ : i ∈ Finset.univ
h✝ : Nonempty n
x : n → α := fun j ↦ unitOf (A i j)
⊢ ‖fun j ↦ unitOf (A i j)‖₊ = 1
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: case inr
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
i : m
x✝ : i ∈ Finset.univ
h✝ : Nonempty n
x : n → α := fun j ↦ unitOf (A i j)
hxn : ‖x‖₊ = 1
hN : ‖∑ i_1, A i i_1 * x i_1‖₊ ≤ N
⊢ ∑ j, ‖A i j‖₊ ≤ N

Tactic:
x,

Goal state after:
case inr
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : NontriviallyNormedField α
inst✝ : NormedAlgebra ℝ α
A : Matrix m n α
N : ℝ≥0
i : m
x✝ : i ∈ Finset.univ
h✝ : Nonempty n
x : n → α := fun j ↦ unitOf (A i j)
hxn : ‖x‖₊ = 1
hN : ‖∑ x, A i x * unitOf (A i x)‖₊ ≤ N
⊢ ∑ j, ‖A i j‖₊ ≤ N
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✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : s ∈ 𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ i ∈ t, s ∈ 𝓝ˢ (quasispectrum 𝕜 (a i))
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) t

Tactic:
have (x : t) : ∃ S, IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a x), quasispectrum 𝕜 x' ⊆ S) ∧ S ⊆ s := by
    obtain ⟨S, ⟨hS₁, hS₂⟩, hS₃⟩ :=
      quasispectrum.isCompact (𝕜 := 𝕜) (a x) |>.nhdsSet_basis_isCompact.mem_iff.mp (hs' x x.2)
    refine ⟨S, hS₂, ?_, hS₃⟩
    exact upperHemicontinuous_quasispectrum 𝕜 A |>.upperHemicontinuousAt (a x) _ hS₁ |>.mono
      fun _ ↦ subset_of_mem_nhdsSet

Goal state after:
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✝¹ : CompleteSpace A
inst✝ : TopologicalSpace X
s : Set 𝕜
f : 𝕜 → 𝕜
a : X → A
t : Set X
hs : s ∈ 𝓝ˢ (⋃ x ∈ t, quasispectrum 𝕜 (a x))
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, p (a x)
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ i ∈ t, s ∈ 𝓝ˢ (quasispectrum 𝕜 (a i))
this : ∀ (x : ↑t), ∃ S, IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a ↑x), quasispectrum 𝕜 x' ⊆ S) ∧ S ⊆ s
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) t
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: X : Type u_1
A : Type u_2
inst✝¹³ : NonUnitalNormedRing A
inst✝¹² : StarRing A
inst✝¹¹ : NormedSpace ℝ A
inst✝¹⁰ : IsScalarTower ℝ A A
inst✝⁹ : SMulCommClass ℝ A A
inst✝⁸ : ContinuousStar A
inst✝⁷ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
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
t : Set X
hs : s ∈ 𝓝ˢ (⋃ x ∈ t, quasispectrum ℝ≥0 (a x))
ha_cont : ContinuousOn a t
ha' : ∀ x ∈ t, 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
hs' : ∀ i ∈ t, s ∈ 𝓝ˢ (quasispectrum ℝ≥0 (a i))
S : ↑t → Set ℝ≥0
hS₁ : ∀ (x : ↑t), IsCompact (S x)
hS₂ : ∀ (x : ↑t), ∀ᶠ (x' : A) in 𝓝 (a ↑x), quasispectrum ℝ≥0 x' ⊆ S x
hS₃ : ∀ (x : ↑t), S x ⊆ s
⊢ ContinuousOn (fun x ↦ cfcₙ f (a x)) t

Tactic:
refine ha_cont.cfcₙ_nnreal (s := fun x : X ↦ if hx : x ∈ t then S ⟨x, hx⟩ else ∅) f
    (by simpa +contextual using hS₁) ?_ ha' ?_
  all_goals simp +contextual only [↓reduceDIte]
  · exact fun x₀ hx₀ ↦ ha_cont.continuousWithinAt hx₀ |>.eventually <| hS₂ ⟨x₀, hx₀⟩
  · exact fun x hx ↦ hf.mono <| hS₃ ⟨x, hx⟩

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

Goal state before:
pp: case h
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
⊢ j ∈ Finset.univ.val ∧ ‖U i j‖ ^ 2 = ‖U i j‖ ^ 2

Tactic:
simp only [Finset.mem_univ_val, and_self_iff]

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

Goal state before:
pp: case h₁.hs
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e e' : Pretrivialization F proj
h₁ : ∀ (x : Z), ↑e x = ↑e' x
h₂ : ∀ (x : B × F), ↑e.symm x = ↑e'.symm x
h₃ : e.baseSet = e'.baseSet
⊢ e.source = e'.source

Tactic:
· rw [e.source_eq, e'.source_eq, h₃]

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

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
s : Set B
x : B
y : F
h : x ∈ e.baseSet
⊢ proj (↑e.symm (x, y)) ∈ s ↔ x ∈ s

Tactic:
e.proj_symm_apply' h

Goal state after:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
s : Set B
x : B
y : F
h : x ∈ e.baseSet
⊢ x ∈ s ↔ x ∈ s
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 j : ι
x : B
v : F
hx : x ∈ Z.baseSet i ∧ x ∈ Z.baseSet j
⊢ (((x, v).1, Z.coordChange i j (x, v).1 (x, v).2).1,
      Z.coordChange j i ((x, v).1, Z.coordChange i j (x, v).1 (x, v).2).1
        ((x, v).1, Z.coordChange i j (x, v).1 (x, v).2).2) =
    (x, v)

Tactic:
dsimp only

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 j : ι
x : B
v : F
hx : x ∈ Z.baseSet i ∧ x ∈ Z.baseSet j
⊢ (x, Z.coordChange j i x (Z.coordChange i j x v)) = (x, v)
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 j : ι
x : B
v : F
hx : x ∈ Z.baseSet i ∧ x ∈ Z.baseSet j
⊢ (x, Z.coordChange j i x (Z.coordChange i j x v)) = (x, v)

Tactic:
coordChange_comp,

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 j : ι
x : B
v : F
hx : x ∈ Z.baseSet i ∧ x ∈ Z.baseSet j
⊢ (x, Z.coordChange i i x v) = (x, v)

case a
ι : 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 j : ι
x : B
v : F
hx : x ∈ Z.baseSet i ∧ x ∈ Z.baseSet j
⊢ x ∈ Z.baseSet i ∩ Z.baseSet j ∩ Z.baseSet i
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 j : ι
x : B
v : F
hx : x ∈ Z.baseSet i ∧ x ∈ Z.baseSet j
⊢ (((x, v).1, Z.coordChange j i (x, v).1 (x, v).2).1,
      Z.coordChange i j ((x, v).1, Z.coordChange j i (x, v).1 (x, v).2).1
        ((x, v).1, Z.coordChange j i (x, v).1 (x, v).2).2) =
    (x, v)

Tactic:
dsimp only

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 j : ι
x : B
v : F
hx : x ∈ Z.baseSet i ∧ x ∈ Z.baseSet j
⊢ (x, Z.coordChange i j x (Z.coordChange j i x v)) = (x, v)
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 : B
v : Z.Fiber x
hx : x ∈ Z.baseSet i
⊢ {
      proj :=
        ({ proj := x, snd := v }.proj,
            Z.coordChange (Z.indexAt { proj := x, snd := v }.proj) i { proj := x, snd := v }.proj
              { proj := x, snd := v }.snd).1,
      snd :=
        Z.coordChange i
          (Z.indexAt
            ({ proj := x, snd := v }.proj,
                Z.coordChange (Z.indexAt { proj := x, snd := v }.proj) i { proj := x, snd := v }.proj
                  { proj := x, snd := v }.snd).1)
          ({ proj := x, snd := v }.proj,
              Z.coordChange (Z.indexAt { proj := x, snd := v }.proj) i { proj := x, snd := v }.proj
                { proj := x, snd := v }.snd).1
          ({ proj := x, snd := v }.proj,
              Z.coordChange (Z.indexAt { proj := x, snd := v }.proj) i { proj := x, snd := v }.proj
                { proj := x, snd := v }.snd).2 } =
    { proj := x, snd := v }

Tactic:
dsimp only

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 : ι
x : B
v : Z.Fiber x
hx : x ∈ Z.baseSet i
⊢ { proj := x, snd := Z.coordChange i (Z.indexAt x) x (Z.coordChange (Z.indexAt x) i x v) } = { proj := x, snd := v }
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 : B
v : F
hx : x ∈ Z.baseSet i
⊢ ({ proj := (x, v).1, snd := Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2 }.proj,
      Z.coordChange (Z.indexAt { proj := (x, v).1, snd := Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2 }.proj)
        i { proj := (x, v).1, snd := Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2 }.proj
        { proj := (x, v).1, snd := Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2 }.snd) =
    (x, v)

Tactic:
dsimp only

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 : ι
x : B
v : F
hx : x ∈ Z.baseSet i
⊢ (x, Z.coordChange (Z.indexAt x) i x (Z.coordChange i (Z.indexAt x) x v)) = (x, v)
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
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
z : ↑(proj ⁻¹' s)
hz : z ∈ Subtype.val ⁻¹' e.source
⊢ (if h : (↑(⟨proj ↑z, ⋯⟩, (↑e ↑z).2).1, (⟨proj ↑z, ⋯⟩, (↑e ↑z).2).2) ∈ e.target then
      ⟨e.invFun (↑(⟨proj ↑z, ⋯⟩, (↑e ↑z).2).1, (⟨proj ↑z, ⋯⟩, (↑e ↑z).2).2), ⋯⟩
    else Classical.arbitrary (↑s → F → ↑(proj ⁻¹' s)) (⟨proj ↑z, ⋯⟩, (↑e ↑z).2).1 (⟨proj ↑z, ⋯⟩, (↑e ↑z).2).2) =
    z

Tactic:
dsimp only

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
e✝ : Pretrivialization F proj
x : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
z : ↑(proj ⁻¹' s)
hz : z ∈ Subtype.val ⁻¹' e.source
⊢ (if h : (proj ↑z, (↑e ↑z).2) ∈ e.target then ⟨e.invFun (proj ↑z, (↑e ↑z).2), ⋯⟩
    else Classical.arbitrary (↑s → F → ↑(proj ⁻¹' s)) ⟨proj ↑z, ⋯⟩ (↑e ↑z).2) =
    z
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ Continuous[inst✝¹, inst✝¹] (e₁.coordChange e₂ b)

Tactic:
by
  refine continuous_snd.comp (e₂.toOpenPartialHomeomorph.continuousOn.comp_continuous
    (e₁.toOpenPartialHomeomorph.continuousOn_symm.comp_continuous ?_ ?_) ?_)
  · fun_prop
  · exact fun x => e₁.mem_target.2 h₁
  · intro x
    rwa [e₂.mem_source, e₁.proj_symm_apply' h₁]

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
e e' : Trivialization F proj
s : Set B
Hs : e.baseSet ∩ frontier s = e'.baseSet ∩ frontier s
Heq : EqOn (↑e) (↑e') (proj ⁻¹' (e.baseSet ∩ frontier s))
p : Z
⊢ p ∈ (e.piecewise e'.toOpenPartialHomeomorph (proj ⁻¹' s) (s ×ˢ univ) ⋯ ⋯ ⋯ ⋯).source →
    (↑(e.piecewise e'.toOpenPartialHomeomorph (proj ⁻¹' s) (s ×ˢ univ) ⋯ ⋯ ⋯ ⋯) p).1 = proj p

Tactic:
rintro (⟨he, hs⟩ | ⟨he, hs⟩)

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
s : Set B
Hs : e.baseSet ∩ frontier s = e'.baseSet ∩ frontier s
Heq : EqOn (↑e) (↑e') (proj ⁻¹' (e.baseSet ∩ frontier s))
p : Z
he : p ∈ e.source
hs : p ∈ proj ⁻¹' s
⊢ (↑(e.piecewise e'.toOpenPartialHomeomorph (proj ⁻¹' s) (s ×ˢ univ) ⋯ ⋯ ⋯ ⋯) p).1 = proj p

case inr
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
s : Set B
Hs : e.baseSet ∩ frontier s = e'.baseSet ∩ frontier s
Heq : EqOn (↑e) (↑e') (proj ⁻¹' (e.baseSet ∩ frontier s))
p : Z
he : p ∈ e'.source
hs : p ∉ proj ⁻¹' s
⊢ (↑(e.piecewise e'.toOpenPartialHomeomorph (proj ⁻¹' s) (s ×ˢ univ) ⋯ ⋯ ⋯ ⋯) p).1 = proj p
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
g : Y → Z
f : X → Y
s : Set X
hgf : IsLocalHomeomorphOn (g ∘ f) s
hf : IsLocalHomeomorphOn f s
⊢ ∀ x ∈ f '' s, ∃ e, x ∈ e.source ∧ Set.EqOn g (↑e) e.source

Tactic:
by
  rintro _ ⟨x, hx, rfl⟩
  obtain ⟨f, hxf, rfl⟩ := hf x hx
  obtain ⟨gf, hgf, he⟩ := hgf x hx
  refine ⟨f.symm.trans gf, ⟨f.map_source hxf, ?_⟩, fun y hy ↦ ?_⟩
  · apply (f.left_inv hxf).symm ▸ hgf
  · change g y = gf (f.symm y)
    rw [← he, Function.comp_apply, f.right_inv hy.1]

Goal state after:
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsLocalHomeomorph f
⊢ DiscreteTopology ↑(Set.range f) ↔ DiscreteTopology X

Tactic:
by
  rw [← Set.image_univ, ← (Homeomorph.Set.univ X).discreteTopology_iff]
  exact h.isLocalHomeomorphOn.discreteTopology_image_iff isOpen_univ

Goal state after: