Theorem: Units.coe_val_inv (FltRegular/NumberTheory/Hilbert92.lean)

State before:
p : ℕ+
K : Type u_1
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
k : Type u_2
inst✝¹⁴ : Field k
inst✝¹³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹² : AddCommGroup G
inst✝¹¹ : CommGroup H
inst✝¹⁰ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁹ : DistribMulAction H G
inst✝⁸ : Module.Free ℤ G
inst✝⁷ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝⁶ : Algebra k K
inst✝⁵ : IsGalois k K
inst✝⁴ : FiniteDimensional k K
inst✝³ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
S : Type u_6
inst✝² : DivisionMonoid M
inst✝¹ : SetLike S M
inst✝ : SubmonoidClass S M
s : S
v : (↥s)ˣ
⊢ (↑↑v)⁻¹ = ↑↑v⁻¹
Tactic:
apply inv_eq_of_mul_eq_one_right
State after:
case a
p : ℕ+
K : Type u_1
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
k : Type u_2
inst✝¹⁴ : Field k
inst✝¹³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹² : AddCommGroup G
inst✝¹¹ : CommGroup H
inst✝¹⁰ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁹ : DistribMulAction H G
inst✝⁸ : Module.Free ℤ G
inst✝⁷ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝⁶ : Algebra k K
inst✝⁵ : IsGalois k K
inst✝⁴ : FiniteDimensional k K
inst✝³ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
S : Type u_6
inst✝² : DivisionMonoid M
inst✝¹ : SetLike S M
inst✝ : SubmonoidClass S M
s : S
v : (↥s)ˣ
⊢ ↑↑v * ↑↑v⁻¹ = 1

State before:
case a
p : ℕ+
K : Type u_1
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
k : Type u_2
inst✝¹⁴ : Field k
inst✝¹³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹² : AddCommGroup G
inst✝¹¹ : CommGroup H
inst✝¹⁰ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁹ : DistribMulAction H G
inst✝⁸ : Module.Free ℤ G
inst✝⁷ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝⁶ : Algebra k K
inst✝⁵ : IsGalois k K
inst✝⁴ : FiniteDimensional k K
inst✝³ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
S : Type u_6
inst✝² : DivisionMonoid M
inst✝¹ : SetLike S M
inst✝ : SubmonoidClass S M
s : S
v : (↥s)ˣ
⊢ ↑↑v * ↑↑v⁻¹ = 1
Tactic:
show ((v * v⁻¹ : _) : M) = 1
State after:
case a
p : ℕ+
K : Type u_1
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
k : Type u_2
inst✝¹⁴ : Field k
inst✝¹³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹² : AddCommGroup G
inst✝¹¹ : CommGroup H
inst✝¹⁰ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁹ : DistribMulAction H G
inst✝⁸ : Module.Free ℤ G
inst✝⁷ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝⁶ : Algebra k K
inst✝⁵ : IsGalois k K
inst✝⁴ : FiniteDimensional k K
inst✝³ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
S : Type u_6
inst✝² : DivisionMonoid M
inst✝¹ : SetLike S M
inst✝ : SubmonoidClass S M
s : S
v : (↥s)ˣ
⊢ ↑↑(v * v⁻¹) = 1

State before:
case a
p : ℕ+
K : Type u_1
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
k : Type u_2
inst✝¹⁴ : Field k
inst✝¹³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹² : AddCommGroup G
inst✝¹¹ : CommGroup H
inst✝¹⁰ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁹ : DistribMulAction H G
inst✝⁸ : Module.Free ℤ G
inst✝⁷ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝⁶ : Algebra k K
inst✝⁵ : IsGalois k K
inst✝⁴ : FiniteDimensional k K
inst✝³ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
S : Type u_6
inst✝² : DivisionMonoid M
inst✝¹ : SetLike S M
inst✝ : SubmonoidClass S M
s : S
v : (↥s)ˣ
⊢ ↑↑(v * v⁻¹) = 1
Tactic:
rw [mul_inv_self]
State after:
case a
p : ℕ+
K : Type u_1
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
k : Type u_2
inst✝¹⁴ : Field k
inst✝¹³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹² : AddCommGroup G
inst✝¹¹ : CommGroup H
inst✝¹⁰ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁹ : DistribMulAction H G
inst✝⁸ : Module.Free ℤ G
inst✝⁷ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝⁶ : Algebra k K
inst✝⁵ : IsGalois k K
inst✝⁴ : FiniteDimensional k K
inst✝³ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
S : Type u_6
inst✝² : DivisionMonoid M
inst✝¹ : SetLike S M
inst✝ : SubmonoidClass S M
s : S
v : (↥s)ˣ
⊢ ↑↑1 = 1

State before:
case a
p : ℕ+
K : Type u_1
inst✝¹⁶ : Field K
inst✝¹⁵ : NumberField K
k : Type u_2
inst✝¹⁴ : Field k
inst✝¹³ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹² : AddCommGroup G
inst✝¹¹ : CommGroup H
inst✝¹⁰ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r : ℕ
inst✝⁹ : DistribMulAction H G
inst✝⁸ : Module.Free ℤ G
inst✝⁷ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝⁶ : Algebra k K
inst✝⁵ : IsGalois k K
inst✝⁴ : FiniteDimensional k K
inst✝³ : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
S : Type u_6
inst✝² : DivisionMonoid M
inst✝¹ : SetLike S M
inst✝ : SubmonoidClass S M
s : S
v : (↥s)ˣ
⊢ ↑↑1 = 1
Tactic:
rfl
State after:
no goals