-- Mathlib/RingTheory/Valuation/ValuationRing.lean
theorem mem_integer_iff (x : K) : x ∈ (valuation A K).integer ↔ ∃ a : A, algebraMap A K a = x

Proof state:
case mpr.intro
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
c : A
⊢ (algebraMap A K) c ∈ (valuation A K).integer

Tactic:
use c

Result:
case h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
c : A
⊢ c • 1 = (algebraMap A K) c

Proof state:
case mpr
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
x : K
⊢ (∃ a, (algebraMap A K) a = x) → x ∈ (valuation A K).integer

Tactic:
rintro ⟨c, rfl⟩

Result:
case mpr.intro
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
c : A
⊢ (algebraMap A K) c ∈ (valuation A K).integer

Proof state:
case h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
c : A
⊢ c • 1 = (algebraMap A K) c

Tactic:
rw [Algebra.smul_def, mul_one]

Result:
no goals

Proof state:
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
x : K
⊢ x ∈ (valuation A K).integer ↔ ∃ a, (algebraMap A K) a = x

Tactic:
constructor

Result:
case mp
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
x : K
⊢ x ∈ (valuation A K).integer → ∃ a, (algebraMap A K) a = x

case mpr
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
x : K
⊢ (∃ a, (algebraMap A K) a = x) → x ∈ (valuation A K).integer

Proof state:
case mp.intro
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
c : A
⊢ ∃ a, (algebraMap A K) a = c • 1

Tactic:
use c

Result:
case h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
c : A
⊢ (algebraMap A K) c = c • 1

Proof state:
case h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
c : A
⊢ (algebraMap A K) c = c • 1

Tactic:
rw [Algebra.smul_def, mul_one]

Result:
no goals

Proof state:
case mp
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
x : K
⊢ x ∈ (valuation A K).integer → ∃ a, (algebraMap A K) a = x

Tactic:
rintro ⟨c, rfl⟩

Result:
case mp.intro
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
c : A
⊢ ∃ a, (algebraMap A K) a = c • 1