-- Mathlib/RingTheory/Algebraic/Integral.lean
theorem exists_integral_multiple (hz : IsAlgebraic R z) : ∃ y ≠ (0 : R), IsIntegral R (y • z)

Proof state:
case pos
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective ⇑(algebraMap R A)
p : R[X]
p_ne_zero : p ≠ 0
px : (aeval z) p = 0
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Tactic:
set a := p.leadingCoeff

Result:
case pos
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective ⇑(algebraMap R A)
p : R[X]
p_ne_zero : p ≠ 0
px : (aeval z) p = 0
a : R := p.leadingCoeff
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Proof state:
case pos
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective ⇑(algebraMap R A)
p : R[X]
p_ne_zero : p ≠ 0
px : (aeval z) p = 0
a : R := p.leadingCoeff
a_ne_zero : a ≠ 0
x_integral : IsIntegral R ((algebraMap R A) a * z)
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Tactic:
exact ⟨_, a_ne_zero, Algebra.smul_def a z ▸ x_integral⟩

Result:
no goals

Proof state:
case pos
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective ⇑(algebraMap R A)
p : R[X]
p_ne_zero : p ≠ 0
px : (aeval z) p = 0
a : R := p.leadingCoeff
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Tactic:
have a_ne_zero : a ≠ 0 := mt Polynomial.leadingCoeff_eq_zero.mp p_ne_zero

Result:
case pos
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective ⇑(algebraMap R A)
p : R[X]
p_ne_zero : p ≠ 0
px : (aeval z) p = 0
a : R := p.leadingCoeff
a_ne_zero : a ≠ 0
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Proof state:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ∃ a, (algebraMap R A) a = 0 ∧ a ≠ 0
r : R
eq : (algebraMap R A) r = 0
ne : r ≠ 0
⊢ IsIntegral R (r • z)

Tactic:
simpa [← algebraMap_smul A, eq, zero_smul] using isIntegral_zero

Result:
no goals

Proof state:
case pos
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective ⇑(algebraMap R A)
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Tactic:
have ⟨p, p_ne_zero, px⟩ := hz

Result:
case pos
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective ⇑(algebraMap R A)
p : R[X]
p_ne_zero : p ≠ 0
px : (aeval z) p = 0
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Proof state:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Tactic:
by_cases inj : Function.Injective (algebraMap R A)

Result:
case pos
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective ⇑(algebraMap R A)
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

case neg
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ¬Function.Injective ⇑(algebraMap R A)
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Proof state:
case neg
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ∃ a, (algebraMap R A) a = 0 ∧ a ≠ 0
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Tactic:
have ⟨r, eq, ne⟩ := inj

Result:
case neg
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ∃ a, (algebraMap R A) a = 0 ∧ a ≠ 0
r : R
eq : (algebraMap R A) r = 0
ne : r ≠ 0
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Proof state:
case neg
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ∃ a, (algebraMap R A) a = 0 ∧ a ≠ 0
r : R
eq : (algebraMap R A) r = 0
ne : r ≠ 0
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Tactic:
exact ⟨r, ne, by simpa [← algebraMap_smul A, eq, zero_smul] using isIntegral_zero⟩

Result:
no goals

Proof state:
case neg
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ¬∀ (a : R), (algebraMap R A) a = 0 → a = 0
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Tactic:
push_neg at inj

Result:
case neg
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ∃ a, (algebraMap R A) a = 0 ∧ a ≠ 0
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Proof state:
case neg
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ¬Function.Injective ⇑(algebraMap R A)
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Tactic:
rw [injective_iff_map_eq_zero] at inj

Result:
case neg
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ¬∀ (a : R), (algebraMap R A) a = 0 → a = 0
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Proof state:
case pos
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective ⇑(algebraMap R A)
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

case neg
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ¬Function.Injective ⇑(algebraMap R A)
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Tactic:
swap

Result:
case neg
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ¬Function.Injective ⇑(algebraMap R A)
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

case pos
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective ⇑(algebraMap R A)
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Proof state:
case pos
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective ⇑(algebraMap R A)
p : R[X]
p_ne_zero : p ≠ 0
px : (aeval z) p = 0
a : R := p.leadingCoeff
a_ne_zero : a ≠ 0
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)

Tactic:
have x_integral : IsIntegral R (algebraMap R A a * z) :=
  ⟨p.integralNormalization, monic_integralNormalization p_ne_zero,
    integralNormalization_aeval_eq_zero px fun _ ↦ (map_eq_zero_iff _ inj).mp⟩

Result:
case pos
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective ⇑(algebraMap R A)
p : R[X]
p_ne_zero : p ≠ 0
px : (aeval z) p = 0
a : R := p.leadingCoeff
a_ne_zero : a ≠ 0
x_integral : IsIntegral R ((algebraMap R A) a * z)
⊢ ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)