mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
h : f.ker = ⊥
g : U ≃ₗ[𝕜] ↥f.range := LinearEquiv.ofBijective f.rangeRestrict ⋯
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range := ⋯ ▸ stdOrthonormalBasis 𝕜 ↥f.range
this :
  ((toMatrix bv.toBasis bu.toBasis) (adjoint f.rangeRestrict)).det *
      ((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det ≠
    0
⊢ ¬((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det = 0

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
h : f.ker = ⊥
g : U ≃ₗ[𝕜] ↥f.range := LinearEquiv.ofBijective f.rangeRestrict ⋯
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range := ⋯ ▸ stdOrthonormalBasis 𝕜 ↥f.range
this :
  ((toMatrix bv.toBasis bu.toBasis) (adjoint f.rangeRestrict)).det *
      ((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det ≠
    0
⊢ ¬((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det = 0
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
h : f.ker = ⊥
g : U ≃ₗ[𝕜] ↥f.range := LinearEquiv.ofBijective f.rangeRestrict ⋯
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range := ⋯ ▸ stdOrthonormalBasis 𝕜 ↥f.range
⊢ ((toMatrix bv.toBasis bu.toBasis) (adjoint f.rangeRestrict)).det *
      ((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det ≠
    0

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
h : f.ker = ⊥
g : U ≃ₗ[𝕜] ↥f.range := LinearEquiv.ofBijective f.rangeRestrict ⋯
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range := ⋯ ▸ stdOrthonormalBasis 𝕜 ↥f.range
⊢ f.ker = ⊥
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
b : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range
⊢ finrank 𝕜 ↥f.range = finrank 𝕜 U

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
b : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range
⊢ finrank 𝕜 ↥f.range = finrank 𝕜 U
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
b : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range
hrank : finrank 𝕜 ↥f.range = finrank 𝕜 U
⊢ f.ker = ⊥

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
b : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range
hrank : finrank 𝕜 ↥f.range = finrank 𝕜 U
⊢ f.ker = ⊥
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
tfae_1_iff_2 : f.normDet ≠ 0 ↔ f.ker = ⊥
tfae_1_iff_3 : f.normDet ≠ 0 ↔ finrank 𝕜 ↥f.range = finrank 𝕜 U
tfae_3_to_4 : finrank 𝕜 ↥f.range = finrank 𝕜 U → Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)
b : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range
⊢ finrank 𝕜 ↥f.range = finrank 𝕜 U

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
tfae_1_iff_2 : f.normDet ≠ 0 ↔ f.ker = ⊥
tfae_1_iff_3 : f.normDet ≠ 0 ↔ finrank 𝕜 ↥f.range = finrank 𝕜 U
tfae_3_to_4 : finrank 𝕜 ↥f.range = finrank 𝕜 U → Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)
b : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range
⊢ finrank 𝕜 ↥f.range = finrank 𝕜 U
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, HolderOnWith C r f s
x : X
x✝ : x ∈ univ
⊢ ∃ C, ∃ t ∈ 𝓝[univ] x, HolderOnWith C r f t

Tactic:
simpa using

Goal state after:
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
r : ℝ≥0
f : X → Y
hr : 0 < r
hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, HolderOnWith C r f s
x : X
x✝ : x ∈ univ
⊢ ∃ C, ∃ t ∈ 𝓝 x, HolderOnWith C r f t
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
K : ℝ≥0
f : X → Y
s : Set X
h : LipschitzOnWith K f s
⊢ dimH (f '' s) ≤ dimH s

Tactic:
simpa using

Goal state after:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
K : ℝ≥0
f : X → Y
s : Set X
h : LipschitzOnWith K f s
⊢ dimH (f '' s) ≤ dimH s
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
f : X → Y
s : Set X
hf : ∀ x ∈ s, ∃ C, ∃ t ∈ 𝓝[s] x, LipschitzOnWith C f t
⊢ ∀ x ∈ s, ∃ C, ∃ t ∈ 𝓝[s] x, HolderOnWith C 1 f t

Tactic:
simpa using

Goal state after:
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
f : X → Y
s : Set X
hf : ∀ x ∈ s, ∃ C, ∃ t ∈ 𝓝[s] x, LipschitzOnWith C f t
⊢ ∀ x ∈ s, ∃ C, ∃ t ∈ 𝓝[s] x, LipschitzOnWith C f t
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
f : X → Y
s : Set X
hf : ∀ x ∈ s, ∃ C, ∃ t ∈ 𝓝[s] x, LipschitzOnWith C f t
this : ∀ x ∈ s, ∃ C, ∃ t ∈ 𝓝[s] x, HolderOnWith C 1 f t
⊢ dimH (f '' s) ≤ dimH s

Tactic:
simpa using

Goal state after:
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
f : X → Y
s : Set X
hf : ∀ x ∈ s, ∃ C, ∃ t ∈ 𝓝[s] x, LipschitzOnWith C f t
this : ∀ x ∈ s, ∃ C, ∃ t ∈ 𝓝[s] x, HolderOnWith C 1 f t
⊢ dimH (f '' s) ≤ dimH s
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
tfae_1_iff_2 : f.normDet = 0 ↔ f.ker ≠ ⊥
tfae_1_iff_3 : f.normDet = 0 ↔ finrank 𝕜 ↥f.range ≠ finrank 𝕜 U
⊢ finrank 𝕜 ↥f.range ≠ finrank 𝕜 U ↔ finrank 𝕜 ↥f.range < finrank 𝕜 U

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
tfae_1_iff_2 : f.normDet = 0 ↔ f.ker ≠ ⊥
tfae_1_iff_3 : f.normDet = 0 ↔ finrank 𝕜 ↥f.range ≠ finrank 𝕜 U
⊢ finrank 𝕜 ↥f.range ≤ finrank 𝕜 U
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
f : X → Y
hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, LipschitzOnWith C f s
x : X
x✝ : x ∈ univ
⊢ ∃ C, ∃ t ∈ 𝓝[univ] x, LipschitzOnWith C f t

Tactic:
simpa using

Goal state after:
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
f : X → Y
hf : ∀ (x : X), ∃ C, ∃ s ∈ 𝓝 x, LipschitzOnWith C f s
x : X
x✝ : x ∈ univ
⊢ ∃ C, ∃ t ∈ 𝓝 x, LipschitzOnWith C f t
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
tfae_1_iff_2 : f.normDet = 0 ↔ f.ker ≠ ⊥
tfae_1_iff_3 : f.normDet = 0 ↔ finrank 𝕜 ↥f.range ≠ finrank 𝕜 U
tfae_3_iff_4 : finrank 𝕜 ↥f.range ≠ finrank 𝕜 U ↔ finrank 𝕜 ↥f.range < finrank 𝕜 U
h : ¬finrank 𝕜 ↥f.range = finrank 𝕜 U ↔ ¬Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)
⊢ finrank 𝕜 ↥f.range ≠ finrank 𝕜 U ↔ IsEmpty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
tfae_1_iff_2 : f.normDet = 0 ↔ f.ker ≠ ⊥
tfae_1_iff_3 : f.normDet = 0 ↔ finrank 𝕜 ↥f.range ≠ finrank 𝕜 U
tfae_3_iff_4 : finrank 𝕜 ↥f.range ≠ finrank 𝕜 U ↔ finrank 𝕜 ↥f.range < finrank 𝕜 U
h : ¬finrank 𝕜 ↥f.range = finrank 𝕜 U ↔ ¬Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)
⊢ ¬finrank 𝕜 ↥f.range = finrank 𝕜 U ↔ IsEmpty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] F
s : Set E
⊢ dimH s ≤ dimH (⇑e '' s)

Tactic:
simpa using

Goal state after:
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] F
s : Set E
⊢ dimH s ≤ dimH (⇑e '' s)
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 V
this : FiniteDimensional 𝕜 V
hdet : ¬‖((toMatrix bu.toBasis bv.toBasis) f).det‖ = 0
⊢ IsUnit ((toMatrix bu.toBasis bv.toBasis) f).det

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 V
this : FiniteDimensional 𝕜 V
hdet : ¬‖((toMatrix bu.toBasis bv.toBasis) f).det‖ = 0
⊢ ¬((toMatrix bu.toBasis bv.toBasis) f).det = 0
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: case neg
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 V
this : FiniteDimensional 𝕜 V
hdet : ¬‖((toMatrix bu.toBasis bv.toBasis) f).det‖ = 0
h : IsUnit ((toMatrix bu.toBasis bv.toBasis) f).det
f' : U ≃ₗ[𝕜] V := LinearEquiv.ofIsUnitDet h
hf : f.range = ⊤
⊢ finrank 𝕜 U = finrank 𝕜 ↥⊤

Tactic:
simpa using

Goal state after:
case neg
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 V
this : FiniteDimensional 𝕜 V
hdet : ¬‖((toMatrix bu.toBasis bv.toBasis) f).det‖ = 0
h : IsUnit ((toMatrix bu.toBasis bv.toBasis) f).det
f' : U ≃ₗ[𝕜] V := LinearEquiv.ofIsUnitDet h
hf : f.range = ⊤
⊢ finrank 𝕜 U = finrank 𝕜 V
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
b : OuterMeasure X
hb : ∀ (i : ℝ≥0∞), ⨆ (_ : i > 0), ⊤ ≤ b
⊢ ⊤ ≤ b

Tactic:
simpa using

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
b : OuterMeasure X
hb : ∀ (i : ℝ≥0∞), ⨆ (_ : i > 0), ⊤ ≤ b
⊢ b = ⊤
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: case refine_2
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
this : ⇑e '' s ∈ 𝓝 (e x)
r : ℝ
hr0 : 0 < r
hr : Metric.ball (e x) r ⊆ ⇑e '' s
⊢ ↑(finrank ℝ E) ≤ dimH (⇑e '' s)

Tactic:
simpa using

Goal state after:
case refine_2
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
h : s ∈ 𝓝 x
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ
this : ⇑e '' s ∈ 𝓝 (e x)
r : ℝ
hr0 : 0 < r
hr : Metric.ball (e x) r ⊆ ⇑e '' s
⊢ ↑(finrank ℝ E) ≤ dimH (⇑e '' s)
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
c : 𝕜
hc : ¬c = 0
h : ¬f.ker = ⊥
⊢ (c • f).ker ≠ ⊥

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
c : 𝕜
hc : ¬c = 0
h : ¬f.ker = ⊥
⊢ ¬f.ker = ⊥
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
c : 𝕜
⊢ (c • f).normDet = ‖c‖ ^ finrank 𝕜 U * f.normDet

Tactic:
by
  by_cases hc : c = 0
  · nontriviality U
    simp [hc, zero_pow finrank_pos.ne.symm]
  by_cases h : f.ker = ⊥
  · obtain ⟨bv⟩ := (f.normDet_ne_zero_tfae.out 1 3).mp h
    let bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
    let bv' : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 (c • f).range := bv.map
      (LinearIsometryEquiv.ofEq _ _ (LinearMap.range_smul _ _ hc).symm)
    rw [f.normDet_eq_norm_det_toMatrix_rangeRestrict bu bv,
      (c • f).normDet_eq_norm_det_toMatrix_rangeRestrict bu bv', ← norm_pow, ← norm_mul]
    have : finrank 𝕜 U = Fintype.card (Fin (finrank 𝕜 U)) := by simp
    conv in c ^ finrank 𝕜 U => rw [this]
    rw [← Matrix.det_smul, ← map_smul]
    rfl
  · have h' : (c • f).ker ≠ ⊥ := by simpa [f.ker_smul _ hc] using h
    simp [normDet_eq_zero_iff_ker_ne_bot.mpr h, normDet_eq_zero_iff_ker_ne_bot.mpr h']

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

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
⊢ (-f).normDet = f.normDet

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup U
inst✝³ : InnerProductSpace 𝕜 U
inst✝² : FiniteDimensional 𝕜 U
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace 𝕜 V
f : U →ₗ[𝕜] V
⊢ (-f).normDet = f.normDet
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hcvx : Convex ℝ s
hne : s.Nonempty
this : Nonempty ↑s
φ : ↥(affineSpan ℝ s) ≃ᵃⁱ[ℝ] ↥(affineSpan ℝ s).direction := AffineIsometryEquiv.constVSub ℝ ⟨hne.some, ⋯⟩
hs_eq : s = Subtype.val '' Subtype.val ⁻¹' s
⊢ (interior (Subtype.val ⁻¹' s)).Nonempty

Tactic:
simpa using

Goal state after:
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hcvx : Convex ℝ s
hne : s.Nonempty
this : Nonempty ↑s
φ : ↥(affineSpan ℝ s) ≃ᵃⁱ[ℝ] ↥(affineSpan ℝ s).direction := AffineIsometryEquiv.constVSub ℝ ⟨hne.some, ⋯⟩
hs_eq : s = Subtype.val '' Subtype.val ⁻¹' s
⊢ (interior (Subtype.val ⁻¹' s)).Nonempty
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
hrank : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction = 1
hrank' : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ = finrank ℝ V - 1
f : ℝ ≃L[ℝ] ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction :=
  (ContinuousLinearEquiv.toSpanNonzeroSingleton ℝ v hv).trans
    (ContinuousLinearEquiv.ofEq (ℝ ∙ v) (AffineSubspace.mk' p (ℝ ∙ v)).direction ⋯)
hf : MeasurableEmbedding ⇑f
p' : ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⟨p, ⋯⟩
g : ℝ → ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⇑(IsometryEquiv.vaddConst p') ∘ ⇑f
hadd : MeasurableEmbedding ⇑(IsometryEquiv.vaddConst p')
hg : MeasurableEmbedding g
v' : ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction := ⟨v, ⋯⟩
⊢ v' ≠ 0

Tactic:
simpa using

Goal state after:
V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
hrank : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction = 1
hrank' : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ = finrank ℝ V - 1
f : ℝ ≃L[ℝ] ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction :=
  (ContinuousLinearEquiv.toSpanNonzeroSingleton ℝ v hv).trans
    (ContinuousLinearEquiv.ofEq (ℝ ∙ v) (AffineSubspace.mk' p (ℝ ∙ v)).direction ⋯)
hf : MeasurableEmbedding ⇑f
p' : ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⟨p, ⋯⟩
g : ℝ → ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⇑(IsometryEquiv.vaddConst p') ∘ ⇑f
hadd : MeasurableEmbedding ⇑(IsometryEquiv.vaddConst p')
hg : MeasurableEmbedding g
v' : ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction := ⟨v, ⋯⟩
⊢ ¬v = 0
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : InnerProductSpace 𝕜 W
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
hbot : (g ∘ₗ f).ker = ⊥
⊢ f.ker = ⊥

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : InnerProductSpace 𝕜 W
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
hbot : (g ∘ₗ f).ker = ⊥
⊢ f.ker = ⊥
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
β : Type u_4
ι : β → Type u_5
hι : (n : β) → Fintype (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i
m : ℝ≥0∞ → ℝ≥0∞
⊢ (mkMetric m) s ≤ liminf (fun n ↦ ∑ i, m (ediam (t n i))) l

Tactic:
simpa using

Goal state after:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
β : Type u_4
ι : β → Type u_5
hι : (n : β) → Fintype (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i
m : ℝ≥0∞ → ℝ≥0∞
⊢ (mkMetric m) s ≤ liminf (fun n ↦ ∑ i, m (ediam (t n i))) l
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup U
inst✝⁶ : InnerProductSpace 𝕜 U
inst✝⁵ : FiniteDimensional 𝕜 U
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace 𝕜 V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : FiniteDimensional 𝕜 V
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
h : finrank 𝕜 U = finrank 𝕜 V
htop : ¬f.range = ⊤
⊢ f.ker ≠ ⊥

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup U
inst✝⁶ : InnerProductSpace 𝕜 U
inst✝⁵ : FiniteDimensional 𝕜 U
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace 𝕜 V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : FiniteDimensional 𝕜 V
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
h : finrank 𝕜 U = finrank 𝕜 V
htop : ¬f.range = ⊤
⊢ ¬f.range = ⊤
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup U
inst✝⁶ : InnerProductSpace 𝕜 U
inst✝⁵ : FiniteDimensional 𝕜 U
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace 𝕜 V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : FiniteDimensional 𝕜 V
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
h : finrank 𝕜 U = finrank 𝕜 V
htop : ¬f.range = ⊤
hbot : (g ∘ₗ f).ker = ⊥
⊢ f.ker = ⊥

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup U
inst✝⁶ : InnerProductSpace 𝕜 U
inst✝⁵ : FiniteDimensional 𝕜 U
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace 𝕜 V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : FiniteDimensional 𝕜 V
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
h : finrank 𝕜 U = finrank 𝕜 V
htop : ¬f.range = ⊤
hbot : (g ∘ₗ f).ker = ⊥
⊢ f.ker = ⊥
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H : μH[d₂] s ≠ 0 ∧ μH[d₁] s ≠ ∞
c : ℝ≥0
hc : c ≠ 0
this : 0 < ↑c ^ (d₂ - d₁)⁻¹
r : ℝ≥0
hr₀✝ : 0 ≤ ↑r
hrc : ↑r < ↑c ^ (d₂ - d₁)⁻¹
hr₀ : r ≠ 0
⊢ ↑r ≠ 0

Tactic:
simpa using

Goal state after:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H : μH[d₂] s ≠ 0 ∧ μH[d₁] s ≠ ∞
c : ℝ≥0
hc : c ≠ 0
this : 0 < ↑c ^ (d₂ - d₁)⁻¹
r : ℝ≥0
hr₀✝ : 0 ≤ ↑r
hrc : ↑r < ↑c ^ (d₂ - d₁)⁻¹
hr₀ : r ≠ 0
⊢ ¬r = 0
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: U : Type u_5
inst✝² : NormedAddCommGroup U
inst✝¹ : InnerProductSpace ℝ U
inst✝ : FiniteDimensional ℝ U
f : U →ₗ[ℝ] U
⊢ f.normDet = |LinearMap.det f|

Tactic:
simpa using

Goal state after:
U : Type u_5
inst✝² : NormedAddCommGroup U
inst✝¹ : InnerProductSpace ℝ U
inst✝ : FiniteDimensional ℝ U
f : U →ₗ[ℝ] U
⊢ f.normDet = |LinearMap.det f|