-- Mathlib/RingTheory/Algebraic/Integral.lean
theorem _root_.Algebra.IsAlgebraic.exists_integral_multiples [NoZeroDivisors R]
    [alg : Algebra.IsAlgebraic R A] (s : Finset A) :
    ∃ y ≠ (0 : R), ∀ z ∈ s, IsIntegral R (y • z)

Proof state:
R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
r : A → R
hr : ∀ (x : A), r x ≠ 0
int : ∀ (x : A), IsIntegral R (r x • x)
x✝ : A
h : x✝ ∈ s
⊢ IsIntegral R ((∏ x ∈ s, r x) • x✝)

Tactic:
classical rw [← Finset.prod_erase_mul _ _ h, mul_smul]

Result:
R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
r : A → R
hr : ∀ (x : A), r x ≠ 0
int : ∀ (x : A), IsIntegral R (r x • x)
x✝ : A
h : x✝ ∈ s
⊢ IsIntegral R ((∏ x ∈ s.erase x✝, r x) • r x✝ • x✝)

Proof state:
R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
⊢ ∃ y, y ≠ 0 ∧ ∀ z ∈ s, IsIntegral R (y • z)

Tactic:
choose r hr int using fun x ↦ (alg.1 x).exists_integral_multiple

Result:
R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
r : A → R
hr : ∀ (x : A), r x ≠ 0
int : ∀ (x : A), IsIntegral R (r x • x)
⊢ ∃ y, y ≠ 0 ∧ ∀ z ∈ s, IsIntegral R (y • z)

Proof state:
R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
r : A → R
hr : ∀ (x : A), r x ≠ 0
int : ∀ (x : A), IsIntegral R (r x • x)
x✝ : A
h : x✝ ∈ s
⊢ IsIntegral R ((∏ x ∈ s.erase x✝, r x) • r x✝ • x✝)

Tactic:
exact (int _).smul _

Result:
no goals

Proof state:
R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
r : A → R
hr : ∀ (x : A), r x ≠ 0
int : ∀ (x : A), IsIntegral R (r x • x)
x✝ : A
h : x✝ ∈ s
⊢ IsIntegral R ((∏ x ∈ s, r x) • x✝)

Tactic:
rw [← Finset.prod_erase_mul _ _ h, mul_smul]

Result:
R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
r : A → R
hr : ∀ (x : A), r x ≠ 0
int : ∀ (x : A), IsIntegral R (r x • x)
x✝ : A
h : x✝ ∈ s
⊢ IsIntegral R ((∏ x ∈ s.erase x✝, r x) • r x✝ • x✝)

Proof state:
R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
⊢ ∃ y, y ≠ 0 ∧ ∀ z ∈ s, IsIntegral R (y • z)

Tactic:
have := Algebra.IsAlgebraic.nontrivial R A

Result:
R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
⊢ ∃ y, y ≠ 0 ∧ ∀ z ∈ s, IsIntegral R (y • z)

Proof state:
R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
r : A → R
hr : ∀ (x : A), r x ≠ 0
int : ∀ (x : A), IsIntegral R (r x • x)
⊢ ∃ y, y ≠ 0 ∧ ∀ z ∈ s, IsIntegral R (y • z)

Tactic:
refine ⟨∏ x ∈ s, r x, Finset.prod_ne_zero_iff.mpr fun _ _ ↦ hr _, fun _ h ↦ ?_⟩

Result:
R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
r : A → R
hr : ∀ (x : A), r x ≠ 0
int : ∀ (x : A), IsIntegral R (r x • x)
x✝ : A
h : x✝ ∈ s
⊢ IsIntegral R ((∏ x ∈ s, r x) • x✝)