-- Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
theorem neg {x : K_hat R K} (hx : x.IsFiniteAdele) : (-x).IsFiniteAdele

Proof state:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K_hat R K
hx : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, x v ∈ adicCompletionIntegers K v
h : ∀ (v : HeightOneSpectrum R), -x v ∈ adicCompletionIntegers K v ↔ x v ∈ adicCompletionIntegers K v
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, (-x) v ∈ adicCompletionIntegers K v

Tactic:
convert hx using 2 with v

Result:
case h.e'_2.h.a
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K_hat R K
hx : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, x v ∈ adicCompletionIntegers K v
h : ∀ (v : HeightOneSpectrum R), -x v ∈ adicCompletionIntegers K v ↔ x v ∈ adicCompletionIntegers K v
v : HeightOneSpectrum R
⊢ (-x) v ∈ adicCompletionIntegers K v ↔ x v ∈ adicCompletionIntegers K v

Proof state:
case h.e'_2.h.a
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K_hat R K
hx : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, x v ∈ adicCompletionIntegers K v
h : ∀ (v : HeightOneSpectrum R), -x v ∈ adicCompletionIntegers K v ↔ x v ∈ adicCompletionIntegers K v
v : HeightOneSpectrum R
⊢ (-x) v ∈ adicCompletionIntegers K v ↔ x v ∈ adicCompletionIntegers K v

Tactic:
convert h v

Result:
no goals

Proof state:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K_hat R K
hx : x.IsFiniteAdele
⊢ (-x).IsFiniteAdele

Tactic:
rw [IsFiniteAdele] at hx ⊢

Result:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K_hat R K
hx : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, x v ∈ adicCompletionIntegers K v
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, (-x) v ∈ adicCompletionIntegers K v

Proof state:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K_hat R K
hx : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, x v ∈ adicCompletionIntegers K v
⊢ ∀ (v : HeightOneSpectrum R), -x v ∈ adicCompletionIntegers K v ↔ x v ∈ adicCompletionIntegers K v

Tactic:
intro v

Result:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K_hat R K
hx : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, x v ∈ adicCompletionIntegers K v
v : HeightOneSpectrum R
⊢ -x v ∈ adicCompletionIntegers K v ↔ x v ∈ adicCompletionIntegers K v

Proof state:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K_hat R K
hx : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, x v ∈ adicCompletionIntegers K v
v : HeightOneSpectrum R
⊢ -x v ∈ adicCompletionIntegers K v ↔ x v ∈ adicCompletionIntegers K v

Tactic:
rw [mem_adicCompletionIntegers, mem_adicCompletionIntegers, Valuation.map_neg]

Result:
no goals

Proof state:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K_hat R K
hx : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, x v ∈ adicCompletionIntegers K v
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, (-x) v ∈ adicCompletionIntegers K v

Tactic:
have h :
  ∀ v : HeightOneSpectrum R,
    -x v ∈ v.adicCompletionIntegers K ↔ x v ∈ v.adicCompletionIntegers K := by
  intro v
  rw [mem_adicCompletionIntegers, mem_adicCompletionIntegers, Valuation.map_neg]

Result:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K_hat R K
hx : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, x v ∈ adicCompletionIntegers K v
h : ∀ (v : HeightOneSpectrum R), -x v ∈ adicCompletionIntegers K v ↔ x v ∈ adicCompletionIntegers K v
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, (-x) v ∈ adicCompletionIntegers K v