mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := fun n ↦ (i : ι) → Fin ⌈(↑(b i) - ↑(a i)) * ↑n⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) := fun n f ↦ univ.pi fun i ↦ Icc (↑(a i) + ↑↑(f i) / ↑n) (↑(a i) + (↑↑(f i) + 1) / ↑n)
A : Tendsto (fun n ↦ 1 / ↑n) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ 1 / ↑n
n : ℕ
hn : 1 ≤ n
npos : 0 < ↑n
x : ι → ℝ
hx : ∀ (i : ι), ↑(a i) < x i ∧ x i < ↑(b i)
f : γ n := fun i ↦ ⟨⌊(x i - ↑(a i)) * ↑n⌋₊, ⋯⟩
i : ι
⊢ ↑(a i) + (x i - ↑(a i)) * ↑n / ↑n ≤ ↑(a i) + (↑⌊(x i - ↑(a i)) * ↑n⌋₊ + 1) / ↑n

Tactic:
gcongr
          exact (Nat.lt_floor_add_one _).le

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
α : Type u_4
l : Filter α
f : α → E →WOT[𝕜] F
A : E →WOT[𝕜] F
⊢ Tendsto f l (𝓝 A) ↔ ∀ (x : E) (y : F), Tendsto (fun a ↦ ⟪y, (f a) x⟫_𝕜) l (𝓝 ⟪y, A x⟫_𝕜)

Tactic:
[

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
α : Type u_4
l : Filter α
f : α → E →WOT[𝕜] F
A : E →WOT[𝕜] F
⊢ Tendsto f l (𝓝 A) ↔ ∀ (x : E) (y : F), Tendsto (fun a ↦ ⟪y, (f a) x⟫_𝕜) l (𝓝 ⟪y, A x⟫_𝕜)
Module: Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E →WOT[𝕜] F
s : Set α
⊢ ContinuousOn f s ↔ ∀ (x : E) (y : F), ContinuousOn (fun x_1 ↦ ⟪y, (f x_1) x⟫_𝕜) s

Tactic:
[

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E →WOT[𝕜] F
s : Set α
⊢ ContinuousOn f s ↔ ∀ (x : E) (y : F), ContinuousOn (fun x_1 ↦ ⟪y, (f x_1) x⟫_𝕜) s
Module: Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E →WOT[𝕜] F
⊢ Continuous[inst✝, instTopologicalSpace] f ↔
    ∀ (x : E) (y : F), Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x_1 ↦ ⟪y, (f x_1) x⟫_𝕜

Tactic:
[

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E →WOT[𝕜] F
⊢ Continuous[inst✝, instTopologicalSpace] f ↔
    ∀ (x : E) (y : F), Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x_1 ↦ ⟪y, (f x_1) x⟫_𝕜
Module: Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] star

Tactic:
[

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] star
Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : NormedField 𝕜'
inst✝² : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
U : Set F
hU : U ∈ 𝓝 0
V : Set E
hV : V ∈ 𝓝 0
h✝ : IsVonNBounded 𝕜' (⇑f '' V)
r : ℝ
hr : r > 0
x : 𝕜
h : ⇑f '' V ⊆ σ x • U
hx : r < ‖x‖
x_ne : x ≠ 0
this : x⁻¹ • V ⊆ ⇑f ⁻¹' U
⊢ x⁻¹ • V ∈ 𝓝 0

Tactic:
set_smul_mem_nhds_zero_iff (inv_ne_zero x_ne)

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : NormedField 𝕜'
inst✝² : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
U : Set F
hU : U ∈ 𝓝 0
V : Set E
hV : V ∈ 𝓝 0
h✝ : IsVonNBounded 𝕜' (⇑f '' V)
r : ℝ
hr : r > 0
x : 𝕜
h : ⇑f '' V ⊆ σ x • U
hx : r < ‖x‖
x_ne : x ≠ 0
this : x⁻¹ • V ⊆ ⇑f ⁻¹' U
⊢ V ∈ 𝓝 0
Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : NormedField 𝕜'
inst✝² : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : IsTopologicalAddGroup F
f : E →ₛₗ[σ] F
U : Set F
hU : U ∈ 𝓝 0
V : Set E
hV : V ∈ 𝓝 0
h✝ : IsVonNBounded 𝕜' (⇑f '' V)
r : ℝ
hr : r > 0
x : 𝕜
h : ⇑f '' V ⊆ σ x • U
hx : r < ‖x‖
x_ne : x ≠ 0
this : x⁻¹ • V ⊆ ⇑f ⁻¹' U
⊢ x⁻¹ • V ∈ 𝓝 0

Tactic:
rwa [set_smul_mem_nhds_zero_iff (inv_ne_zero x_ne)]

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : NormedField 𝕜'
inst✝² : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : FirstCountableTopology E
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i ↦ b i
bE' : (𝓝 0).HasBasis (fun x ↦ True) fun n ↦ c ^ n • b n
⊢ ContinuousAt (⇑f) 0

Tactic:
[

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : NormedField 𝕜'
inst✝² : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : FirstCountableTopology E
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i ↦ b i
bE' : (𝓝 0).HasBasis (fun x ↦ True) fun n ↦ c ^ n • b n
⊢ ContinuousAt (⇑f) 0
Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : NormedField 𝕜'
inst✝² : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : FirstCountableTopology E
f : E →ₛₗ[σ] F
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i ↦ b i
bE' : (𝓝 0).HasBasis (fun x ↦ True) fun n ↦ c ^ n • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (i : ℕ), u i ∈ c ^ i • b i
hu' : ∀ (i : ℕ), f (u i) ∉ V
h_tendsto : Tendsto (fun n ↦ (c ^ n)⁻¹ • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n ↦ (c ^ n)⁻¹ • u n)
hf : IsVonNBounded 𝕜' (Set.range fun x ↦ (σ c ^ x)⁻¹ • f (u x))
this : Tendsto (fun n ↦ σ c ^ n) atTop (𝓝 0)
⊢ Tendsto (⇑f ∘ u) atTop (𝓝 0)

Tactic:
have := hf.smul_tendsto_zero (.of_forall fun n ↦ Set.mem_range_self n) this

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : NormedField 𝕜'
inst✝² : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : FirstCountableTopology E
f : E →ₛₗ[σ] F
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i ↦ b i
bE' : (𝓝 0).HasBasis (fun x ↦ True) fun n ↦ c ^ n • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (i : ℕ), u i ∈ c ^ i • b i
hu' : ∀ (i : ℕ), f (u i) ∉ V
h_tendsto : Tendsto (fun n ↦ (c ^ n)⁻¹ • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n ↦ (c ^ n)⁻¹ • u n)
hf : IsVonNBounded 𝕜' (Set.range fun x ↦ (σ c ^ x)⁻¹ • f (u x))
this✝ : Tendsto (fun n ↦ σ c ^ n) atTop (𝓝 0)
this : Tendsto ((fun n ↦ σ c ^ n) • fun n ↦ (σ c ^ n)⁻¹ • f (u n)) atTop (𝓝 0)
⊢ Tendsto (⇑f ∘ u) atTop (𝓝 0)
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case «0»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
h : ⟪x, y⟫ = 0
j : Fin 2
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ ⟪![x, y] ((fun i ↦ i) ⟨0, ⋯⟩), ![x, y] j⟫ = 0

Tactic:
fin_cases j

Goal state after:
case «0».«0»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
h : ⟪x, y⟫ = 0
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ ⟪![x, y] ((fun i ↦ i) ⟨0, ⋯⟩), ![x, y] ((fun i ↦ i) ⟨0, ⋯⟩)⟫ = 0

case «0».«1»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
h : ⟪x, y⟫ = 0
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ ⟪![x, y] ((fun i ↦ i) ⟨0, ⋯⟩), ![x, y] ((fun i ↦ i) ⟨1, ⋯⟩)⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case «1»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
h : ⟪x, y⟫ = 0
j : Fin 2
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ ⟪![x, y] ((fun i ↦ i) ⟨1, ⋯⟩), ![x, y] j⟫ = 0

Tactic:
fin_cases j

Goal state after:
case «1».«0»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
h : ⟪x, y⟫ = 0
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ ⟪![x, y] ((fun i ↦ i) ⟨1, ⋯⟩), ![x, y] ((fun i ↦ i) ⟨0, ⋯⟩)⟫ = 0

case «1».«1»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
h : ⟪x, y⟫ = 0
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ ⟪![x, y] ((fun i ↦ i) ⟨1, ⋯⟩), ![x, y] ((fun i ↦ i) ⟨1, ⋯⟩)⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ⟪(InnerProductSpace.toDual ℝ E).symm (LinearMap.toContinuousLinearMap (o.areaForm x)), y⟫ = (o.areaForm x) y

Tactic:
InnerProductSpace.toDual_symm_apply

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (LinearMap.toContinuousLinearMap (o.areaForm x)) y = (o.areaForm x) y
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case «0»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
j : Fin 2
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ ⟪![x, o.rightAngleRotation x] ((fun i ↦ i) ⟨0, ⋯⟩), ![x, o.rightAngleRotation x] j⟫ = 0

Tactic:
fin_cases j

Goal state after:
case «0».«0»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ ⟪![x, o.rightAngleRotation x] ((fun i ↦ i) ⟨0, ⋯⟩), ![x, o.rightAngleRotation x] ((fun i ↦ i) ⟨0, ⋯⟩)⟫ = 0

case «0».«1»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ ⟪![x, o.rightAngleRotation x] ((fun i ↦ i) ⟨0, ⋯⟩), ![x, o.rightAngleRotation x] ((fun i ↦ i) ⟨1, ⋯⟩)⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case «1»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
j : Fin 2
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ ⟪![x, o.rightAngleRotation x] ((fun i ↦ i) ⟨1, ⋯⟩), ![x, o.rightAngleRotation x] j⟫ = 0

Tactic:
fin_cases j

Goal state after:
case «1».«0»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ ⟪![x, o.rightAngleRotation x] ((fun i ↦ i) ⟨1, ⋯⟩), ![x, o.rightAngleRotation x] ((fun i ↦ i) ⟨0, ⋯⟩)⟫ = 0

case «1».«1»
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ ⟪![x, o.rightAngleRotation x] ((fun i ↦ i) ⟨1, ⋯⟩), ![x, o.rightAngleRotation x] ((fun i ↦ i) ⟨1, ⋯⟩)⟫ = 0
Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜₁ E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜₂ F
H : SeparatingDual 𝕜₂ F
A B : E →SWOT[σ] F
h : ∀ (x : E) (y : F⋆), y (A x) = y (B x)
⊢ A = B

Tactic:
[

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜₁ E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜₂ F
H : SeparatingDual 𝕜₂ F
A B : E →SWOT[σ] F
h : ∀ (x : E) (y : F⋆), y (A x) = y (B x)
⊢ A = B
Module: Mathlib.Analysis.Matrix.LDL

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : WellFoundedLT n
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
⊢ lower hS * diag hS * (lower hS)ᴴ = S

Tactic:
by
  rw [LDL.lower, conjTranspose_nonsing_inv, Matrix.mul_assoc,
    Matrix.inv_mul_eq_iff_eq_mul_of_invertible (LDL.lowerInv hS),
    Matrix.mul_inv_eq_iff_eq_mul_of_invertible]
  exact LDL.diag_eq_lowerInv_conj hS

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WeakSpace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
e_dual : StrongDual 𝕜 F ≃ StrongDual 𝕜 E
f : StrongDual 𝕜 E
he : ∀ (f : StrongDual 𝕜 F), ⇑(e_dual f) = ⇑(e.dualMap ↑f)
this : ∀ (g : StrongDual 𝕜 E), ⇑g = ⇑(e_dual.symm g) ∘ ⇑e
x : F
| f (e.symm x)

Tactic:
this

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
e_dual : StrongDual 𝕜 F ≃ StrongDual 𝕜 E
f : StrongDual 𝕜 E
he : ∀ (f : StrongDual 𝕜 F), ⇑(e_dual f) = ⇑(e.dualMap ↑f)
this : ∀ (g : StrongDual 𝕜 E), ⇑g = ⇑(e_dual.symm g) ∘ ⇑e
x : F
| (⇑(e_dual.symm f) ∘ ⇑e) (e.symm x)
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s a : ℂ
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (s - 1) • ↑t ^ a • f t = ↑t ^ (s + a - 1) • f t

Tactic:
[

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s a : ℂ
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (s - 1) • ↑t ^ a • f t = ↑t ^ (s + a - 1) • f t
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
⊢ cexp (-s * ↑u) • f (rexp (-u)) = cexp (-↑s.im * ↑u * I) • rexp (-s.re * u) • f (rexp (-u))

pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
⊢ cexp (-↑s.im * ↑u * I) • rexp (-s.re * u) • f (rexp (-u)) =
    cexp (↑(-2 * π * (u * (s.im / (2 * π)))) * I) • rexp (-s.re * u) • f (rexp (-u))

Tactic:
· conv => lhs; rw [← re_add_im s]
        rw [neg_add, add_mul, Complex.exp_add, mul_comm, ← smul_eq_mul, smul_assoc]
        norm_cast
        push_cast
        ring_nf

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
⊢ cexp (-↑s.im * ↑u * I) • rexp (-s.re * u) • f (rexp (-u)) =
    cexp (↑(-2 * π * (u * (s.im / (2 * π)))) * I) • rexp (-s.re * u) • f (rexp (-u))
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
hx0 : ↑x ≠ 0
⊢ |(2 * π)⁻¹| • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * I)) • f (↑σ + ↑y * I) =
    ↑x ^ (-↑σ) • ∫ (y : ℝ), cexp (2 * ↑π * (↑y * -↑(Real.log x)) * I) • f (↑σ + 2 * ↑π * ↑y * I)

Tactic:
[

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
hx0 : ↑x ≠ 0
⊢ |(2 * π)⁻¹| • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * I)) • f (↑σ + ↑y * I) =
    ↑x ^ (-↑σ) • ∫ (y : ℝ), cexp (2 * ↑π * (↑y * -↑(Real.log x)) * I) • f (↑σ + 2 * ↑π * ↑y * I)
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
hx0 : ↑x ≠ 0
⊢ |(2 * π)⁻¹| • ∫ (y : ℝ), ↑x ^ (-↑σ + -(↑y * I)) • f (↑σ + ↑y * I) =
    ↑x ^ (-↑σ) • ∫ (y : ℝ), cexp (2 * ↑π * (↑y * -↑(Real.log x)) * I) • f (↑σ + 2 * ↑π * ↑y * I)

Tactic:
cpow_add _ _ hx0,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
hx0 : ↑x ≠ 0
⊢ |(2 * π)⁻¹| • ∫ (y : ℝ), (↑x ^ (-↑σ) * ↑x ^ (-(↑y * I))) • f (↑σ + ↑y * I) =
    ↑x ^ (-↑σ) • ∫ (y : ℝ), cexp (2 * ↑π * (↑y * -↑(Real.log x)) * I) • f (↑σ + 2 * ↑π * ↑y * I)
Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

Goal state before:
pp: 𝕜₁✝ : Type u_1
𝕜₂✝ : Type u_2
inst✝³¹ : NormedField 𝕜₁✝
inst✝³⁰ : NormedField 𝕜₂✝
σ : 𝕜₁✝ →+* 𝕜₂✝
E✝ : Type u_3
F✝ : Type u_4
inst✝²⁹ : AddCommGroup E✝
inst✝²⁸ : TopologicalSpace E✝
inst✝²⁷ : Module 𝕜₁✝ E✝
inst✝²⁶ : AddCommGroup F✝
inst✝²⁵ : TopologicalSpace F✝
inst✝²⁴ : Module 𝕜₂✝ F✝
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
𝕜₄ : Type u_8
E : Type u_9
F : Type u_10
G : Type u_11
H : Type u_12
inst✝²³ : NormedField 𝕜₁
inst✝²² : NormedField 𝕜₂
inst✝²¹ : NormedField 𝕜₃
inst✝²⁰ : NormedField 𝕜₄
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₁₄ : 𝕜₁ →+* 𝕜₄
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₃₄ : 𝕜₃ →+* 𝕜₄
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁸ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁶ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : Module 𝕜₁ E
inst✝¹² : AddCommGroup F
inst✝¹¹ : TopologicalSpace F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : AddCommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : AddCommGroup H
inst✝⁵ : TopologicalSpace H
inst✝⁴ : Module 𝕜₄ H
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜₂ F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
x✝ : F →WOT[𝕜₂] F
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun x ↦ x✝ * x

Tactic:
[

Goal state after:
𝕜₁✝ : Type u_1
𝕜₂✝ : Type u_2
inst✝³¹ : NormedField 𝕜₁✝
inst✝³⁰ : NormedField 𝕜₂✝
σ : 𝕜₁✝ →+* 𝕜₂✝
E✝ : Type u_3
F✝ : Type u_4
inst✝²⁹ : AddCommGroup E✝
inst✝²⁸ : TopologicalSpace E✝
inst✝²⁷ : Module 𝕜₁✝ E✝
inst✝²⁶ : AddCommGroup F✝
inst✝²⁵ : TopologicalSpace F✝
inst✝²⁴ : Module 𝕜₂✝ F✝
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
𝕜₄ : Type u_8
E : Type u_9
F : Type u_10
G : Type u_11
H : Type u_12
inst✝²³ : NormedField 𝕜₁
inst✝²² : NormedField 𝕜₂
inst✝²¹ : NormedField 𝕜₃
inst✝²⁰ : NormedField 𝕜₄
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₁₄ : 𝕜₁ →+* 𝕜₄
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₃₄ : 𝕜₃ →+* 𝕜₄
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁸ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁶ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : Module 𝕜₁ E
inst✝¹² : AddCommGroup F
inst✝¹¹ : TopologicalSpace F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : AddCommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : AddCommGroup H
inst✝⁵ : TopologicalSpace H
inst✝⁴ : Module 𝕜₄ H
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜₂ F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
x✝ : F →WOT[𝕜₂] F
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] fun x ↦ x✝ * x
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: f : ℝ → ℂ
s a : ℂ
⊢ mellin (fun t ↦ f t / a) s = mellin f s / a

Tactic:
[

Goal state after:
f : ℝ → ℂ
s a : ℂ
⊢ mellin (fun t ↦ f t / a) s = mellin f s / a
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
h2π : 2 * π ≠ 0
this : Integrable (𝓕 fun u ↦ rexp (-(σ * u)) • f (rexp (-u))) volume
⊢ Integrable (𝓕 g) volume

Tactic:
[

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
h2π : 2 * π ≠ 0
this : Integrable (𝓕 fun u ↦ rexp (-(σ * u)) • f (rexp (-u))) volume
⊢ Integrable (𝓕 g) volume
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
⊢ mellin (fun t ↦ f (t ^ a)) s = |a|⁻¹ • mellin f (s / ↑a)

Tactic:
[

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
⊢ mellin (fun t ↦ f (t ^ a)) s = |a|⁻¹ • mellin f (s / ↑a)