mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inr.inr.inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
xl : Y → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
hgb : ∀ (y : Y), g y ≤ b
hb' : ¬∃ x, f x = b
hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {b})
dg : Y →ᵇ ℝ
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Iic c)
dgb : EqOn (⇑dg) (Function.const Y (b - c)) (⇑g ⁻¹' {b})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (b - c)
hgf : ∀ (x : X), (g - dg) (e x) = f x
y : Y
hyb : (g - dg) y < b
xu : X
hyxu : (g - dg) y < f xu
right✝ : f xu ≤ b
hc : g y ≤ c
⊢ ∃ x₁ x₂, (g - dg) y ∈ Icc (f x₁) (f x₂)

Tactic:
·

Goal state after:
case inr.inr.inr
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
xl : Y → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
hgb : ∀ (y : Y), g y ≤ b
hb' : ¬∃ x, f x = b
hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {b})
dg : Y →ᵇ ℝ
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Iic c)
dgb : EqOn (⇑dg) (Function.const Y (b - c)) (⇑g ⁻¹' {b})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (b - c)
hgf : ∀ (x : X), (g - dg) (e x) = f x
y : Y
hyb : (g - dg) y < b
xu : X
hyxu : (g - dg) y < f xu
right✝ : f xu ≤ b
hc : g y ≤ c
⊢ ∃ x₁ x₂, (g - dg) y ∈ Icc (f x₁) (f x₂)
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝¹ : Nontrivial R
a✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝ : Infinite ιS
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

pp: case inl
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝¹ : Nontrivial R
a✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝ : Fintype ιS
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

Tactic:
·

Goal state after:
case inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝¹ : Nontrivial R
a✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝ : Infinite ιS
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h✝ : IsEmpty X
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f

pp: case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h✝ : Nonempty X
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f

Tactic:
·

Goal state after:
case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h✝ : IsEmpty X
⊢ ∃ g, (∀ (y : Y), g y ∈ t) ∧ ⇑g ∘ e = ⇑f
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case e'_2
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
⊢ f w = (f ∘ ↑ofComplex) ↑w

pp: case convert_1
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
⊢ IsPreconnected {z | 0 < z.im}

pp: case convert_2
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
⊢ ∃ᶠ (z : ℂ) in 𝓝[≠] ↑τ, (f ∘ ↑ofComplex) z = 0

Tactic:
·

Goal state after:
case e'_2
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
⊢ f w = (f ∘ ↑ofComplex) ↑w
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case inl.inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝¹ : Nontrivial R
a✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝¹ : Fintype ιS
val✝ : Infinite ιA
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

pp: case inl.inl
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝¹ : Nontrivial R
a✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝¹ : Fintype ιS
val✝ : Fintype ιA
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

Tactic:
·

Goal state after:
case inl.inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝¹ : Nontrivial R
a✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝¹ : Fintype ιS
val✝ : Infinite ιA
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case convert_1
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
⊢ IsPreconnected {z | 0 < z.im}

pp: case convert_2
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
⊢ ∃ᶠ (z : ℂ) in 𝓝[≠] ↑τ, (f ∘ ↑ofComplex) z = 0

Tactic:
·

Goal state after:
case convert_1
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
⊢ IsPreconnected {z | 0 < z.im}
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case convert_2
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
⊢ ∃ᶠ (z : ℂ) in 𝓝[≠] ↑τ, (f ∘ ↑ofComplex) z = 0

Tactic:
·

Goal state after:
case convert_2
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
⊢ ∃ᶠ (z : ℂ) in 𝓝[≠] ↑τ, (f ∘ ↑ofComplex) z = 0
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case neg
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_6
K : Type u_7
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : ¬FiniteDimensional K L
⊢ IsIntegral R ((norm K) x)

pp: case pos
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_6
K : Type u_7
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : FiniteDimensional K L
⊢ IsIntegral R ((norm K) x)

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_6
K : Type u_7
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : ¬FiniteDimensional K L
⊢ IsIntegral R ((norm K) x)
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ := { toFun := Subtype.val ∘ ⇑h ∘ ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ := Subtype.val ∘ ⇑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : t'.OrdConnected
hFt : ∀ (x : X), F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), G y ∈ t'
hGF : ⇑G ∘ e = ⇑F
g : C(Y, ℝ) := { toFun := ⇑h.symm ∘ Set.codRestrict (⇑G) (Ioo (-1) 1) ⋯, continuous_toFun := ⋯ }
hgG : ∀ {y : Y} {a : ℝ}, g y = a ↔ G y = ↑(h a)
y : Y
⊢ g y ∈ t

pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ := { toFun := Subtype.val ∘ ⇑h ∘ ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ := Subtype.val ∘ ⇑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : t'.OrdConnected
hFt : ∀ (x : X), F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), G y ∈ t'
hGF : ⇑G ∘ e = ⇑F
g : C(Y, ℝ) := { toFun := ⇑h.symm ∘ Set.codRestrict (⇑G) (Ioo (-1) 1) ⋯, continuous_toFun := ⋯ }
hgG : ∀ {y : Y} {a : ℝ}, g y = a ↔ G y = ↑(h a)
⊢ ⇑g ∘ e = ⇑f

Tactic:
·

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ := { toFun := Subtype.val ∘ ⇑h ∘ ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ := Subtype.val ∘ ⇑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : t'.OrdConnected
hFt : ∀ (x : X), F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), G y ∈ t'
hGF : ⇑G ∘ e = ⇑F
g : C(Y, ℝ) := { toFun := ⇑h.symm ∘ Set.codRestrict (⇑G) (Ioo (-1) 1) ⋯, continuous_toFun := ⋯ }
hgG : ∀ {y : Y} {a : ℝ}, g y = a ↔ G y = ↑(h a)
y : Y
⊢ g y ∈ t
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ := { toFun := Subtype.val ∘ ⇑h ∘ ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ := Subtype.val ∘ ⇑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : t'.OrdConnected
hFt : ∀ (x : X), F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), G y ∈ t'
hGF : ⇑G ∘ e = ⇑F
g : C(Y, ℝ) := { toFun := ⇑h.symm ∘ Set.codRestrict (⇑G) (Ioo (-1) 1) ⋯, continuous_toFun := ⋯ }
hgG : ∀ {y : Y} {a : ℝ}, g y = a ↔ G y = ↑(h a)
⊢ ⇑g ∘ e = ⇑f

Tactic:
·

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), f x ∈ t
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ := { toFun := Subtype.val ∘ ⇑h ∘ ⇑f, continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ := Subtype.val ∘ ⇑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : t'.OrdConnected
hFt : ∀ (x : X), F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), G y ∈ t'
hGF : ⇑G ∘ e = ⇑F
g : C(Y, ℝ) := { toFun := ⇑h.symm ∘ Set.codRestrict (⇑G) (Ioo (-1) 1) ⋯, continuous_toFun := ⋯ }
hgG : ∀ {y : Y} {a : ℝ}, g y = a ↔ G y = ↑(h a)
⊢ ⇑g ∘ e = ⇑f
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case neg
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
⊢ (norm K) x = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L

pp: case pos
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : FiniteDimensional K L
⊢ (norm K) x = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L

Tactic:
·

Goal state after:
case neg
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
⊢ (norm K) x = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case pos
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : IsIntegral K x
⊢ 1 = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L

pp: case neg
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : ¬IsIntegral K x
⊢ 1 = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L

Tactic:
·

Goal state after:
case pos
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : IsIntegral K x
⊢ 1 = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case neg
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : ¬IsIntegral K x
⊢ 1 = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L

Tactic:
·

Goal state after:
case neg
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : ¬IsIntegral K x
⊢ 1 = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case neg
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : ¬IsIntegral K x
⊢ 1 = 1 ^ finrank (↥K⟮x⟯) L

pp: case neg.h
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : ¬IsIntegral K x
⊢ ¬Module.Finite K ↥K⟮x⟯

Tactic:
·

Goal state after:
case neg
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : ¬IsIntegral K x
⊢ 1 = 1 ^ finrank (↥K⟮x⟯) L
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case neg.h
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : ¬IsIntegral K x
⊢ ¬Module.Finite K ↥K⟮x⟯

Tactic:
·

Goal state after:
case neg.h
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : ¬IsIntegral K x
⊢ ¬Module.Finite K ↥K⟮x⟯
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case e'_9.e'_5
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
⊢ ↑(↑g).det = ↑(↑g 0 0) * 1 * (↑(↑g 1 0) * id ↑τ + ↑(↑g 1 1)) - (↑(↑g 0 0) * id ↑τ + ↑(↑g 0 1)) * (↑(↑g 1 0) * 1)

pp: case convert_5
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
⊢ ↑(↑g 1 0) * id ↑τ + ↑(↑g 1 1) ≠ 0

Tactic:
·

Goal state after:
case e'_9.e'_5
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
⊢ ↑(↑g).det = ↑(↑g 0 0) * 1 * (↑(↑g 1 0) * id ↑τ + ↑(↑g 1 1)) - (↑(↑g 0 0) * id ↑τ + ↑(↑g 0 1)) * (↑(↑g 1 0) * 1)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case convert_5
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
⊢ ↑(↑g 1 0) * id ↑τ + ↑(↑g 1 1) ≠ 0

Tactic:
·

Goal state after:
case convert_5
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
⊢ ↑(↑g 1 0) * id ↑τ + ↑(↑g 1 1) ≠ 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case ha
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
⊢ ↑(↑g).det ≠ 0

pp: case hb
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
⊢ denom g ↑τ ^ 2 ≠ 0

Tactic:
·

Goal state after:
case ha
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
⊢ ↑(↑g).det ≠ 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case hb
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
⊢ denom g ↑τ ^ 2 ≠ 0

Tactic:
·

Goal state after:
case hb
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
⊢ denom g ↑τ ^ 2 ≠ 0
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: L : Type u_6
K : Type u_7
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_9
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsAlgClosed E
x : L
hx : IsIntegral K x
⊢ (∏ σ, σ (adjoin.powerBasis hx).gen) ^ finrank (↥K⟮x⟯) L = ∏ σ, σ x

pp: L : Type u_6
K : Type u_7
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_9
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsAlgClosed E
x : L
hx : IsIntegral K x
⊢ IsSeparable K (adjoin.powerBasis hx).gen

Tactic:
·

Goal state after:
L : Type u_6
K : Type u_7
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_9
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsAlgClosed E
x : L
hx : IsIntegral K x
⊢ (∏ σ, σ (adjoin.powerBasis hx).gen) ^ finrank (↥K⟮x⟯) L = ∏ σ, σ x
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: L : Type u_6
K : Type u_7
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_9
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsAlgClosed E
x : L
hx : IsIntegral K x
⊢ IsSeparable K (adjoin.powerBasis hx).gen

Tactic:
·

Goal state after:
L : Type u_6
K : Type u_7
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_9
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsAlgClosed E
x : L
hx : IsIntegral K x
⊢ IsSeparable K (adjoin.powerBasis hx).gen
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: f : ℍ → ℂ
τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
G : ℂ → ℂ := fun z ↦ ↑(g • ↑ofComplex z)
F : ℂ → ℂ := fun z ↦ f (↑ofComplex z)
this : (fun z ↦ f (g • ↑ofComplex z)) = F ∘ G
⊢ meromorphicOrderAt F (G ↑τ) = meromorphicOrderAt (fun z ↦ f (↑ofComplex z)) ↑(g • τ)

pp: case hg
f : ℍ → ℂ
τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
G : ℂ → ℂ := fun z ↦ ↑(g • ↑ofComplex z)
F : ℂ → ℂ := fun z ↦ f (↑ofComplex z)
this : (fun z ↦ f (g • ↑ofComplex z)) = F ∘ G
⊢ AnalyticAt ℂ G ↑τ

pp: case hg'
f : ℍ → ℂ
τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
G : ℂ → ℂ := fun z ↦ ↑(g • ↑ofComplex z)
F : ℂ → ℂ := fun z ↦ f (↑ofComplex z)
this : (fun z ↦ f (g • ↑ofComplex z)) = F ∘ G
⊢ deriv G ↑τ ≠ 0

Tactic:
·

Goal state after:
f : ℍ → ℂ
τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
G : ℂ → ℂ := fun z ↦ ↑(g • ↑ofComplex z)
F : ℂ → ℂ := fun z ↦ f (↑ofComplex z)
this : (fun z ↦ f (g • ↑ofComplex z)) = F ∘ G
⊢ meromorphicOrderAt F (G ↑τ) = meromorphicOrderAt (fun z ↦ f (↑ofComplex z)) ↑(g • τ)
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: L : Type u_6
K : Type u_7
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ (algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((norm K) x)) = ∏ x, ?f x

pp: case f
L : Type u_6
K : Type u_7
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ (L →ₐ[K] AlgebraicClosure L) → AlgebraicClosure L

pp: case h
L : Type u_6
K : Type u_7
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ ∀ (x_1 : L →ₐ[K] AlgebraicClosure L),
    ?f x_1 = (algebraMap L (AlgebraicClosure L)) (((Normal.algHomEquivAut K (AlgebraicClosure L) L) x_1) x)

Tactic:
·

Goal state after:
L : Type u_6
K : Type u_7
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ (algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((norm K) x)) = ∏ x, ?f x
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case hg
f : ℍ → ℂ
τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
G : ℂ → ℂ := fun z ↦ ↑(g • ↑ofComplex z)
F : ℂ → ℂ := fun z ↦ f (↑ofComplex z)
this : (fun z ↦ f (g • ↑ofComplex z)) = F ∘ G
⊢ AnalyticAt ℂ G ↑τ

pp: case hg'
f : ℍ → ℂ
τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
G : ℂ → ℂ := fun z ↦ ↑(g • ↑ofComplex z)
F : ℂ → ℂ := fun z ↦ f (↑ofComplex z)
this : (fun z ↦ f (g • ↑ofComplex z)) = F ∘ G
⊢ deriv G ↑τ ≠ 0

Tactic:
·

Goal state after:
case hg
f : ℍ → ℂ
τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
G : ℂ → ℂ := fun z ↦ ↑(g • ↑ofComplex z)
F : ℂ → ℂ := fun z ↦ f (↑ofComplex z)
this : (fun z ↦ f (g • ↑ofComplex z)) = F ∘ G
⊢ AnalyticAt ℂ G ↑τ
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case h
L : Type u_6
K : Type u_7
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ ∀ (x_1 : L →ₐ[K] AlgebraicClosure L),
    x_1 x = (algebraMap L (AlgebraicClosure L)) (((Normal.algHomEquivAut K (AlgebraicClosure L) L) x_1) x)

Tactic:
·

Goal state after:
case h
L : Type u_6
K : Type u_7
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ ∀ (x_1 : L →ₐ[K] AlgebraicClosure L),
    x_1 x = (algebraMap L (AlgebraicClosure L)) (((Normal.algHomEquivAut K (AlgebraicClosure L) L) x_1) x)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case hg'
f : ℍ → ℂ
τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
G : ℂ → ℂ := fun z ↦ ↑(g • ↑ofComplex z)
F : ℂ → ℂ := fun z ↦ f (↑ofComplex z)
this : (fun z ↦ f (g • ↑ofComplex z)) = F ∘ G
⊢ deriv G ↑τ ≠ 0

Tactic:
·

Goal state after:
case hg'
f : ℍ → ℂ
τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
G : ℂ → ℂ := fun z ↦ ↑(g • ↑ofComplex z)
F : ℂ → ℂ := fun z ↦ f (↑ofComplex z)
this : (fun z ↦ f (g • ↑ofComplex z)) = F ∘ G
⊢ deriv G ↑τ ≠ 0
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
x : P
⊢ inversion x (dist x x) x = x

pp: case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
hne : x ≠ c
⊢ inversion c (dist x c) x = x

Tactic:
·

Goal state after:
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
x : P
⊢ inversion x (dist x x) x = x
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
hne : x ≠ c
⊢ inversion c (dist x c) x = x

Tactic:
·

Goal state after:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
hne : x ≠ c
⊢ inversion c (dist x c) x = x