-- Mathlib/RingTheory/Adjoin/PowerBasis.lean
theorem repr_pow_isIntegral [IsDomain S] (hB : IsIntegral R B.gen) {x : A}
    (hx : ∀ i, IsIntegral R (B.basis.repr x i))
    (hmin : minpoly S B.gen = (minpoly R B.gen).map (algebraMap R S)) (n : ℕ) :
    ∀ i, IsIntegral R (B.basis.repr (x ^ n) i)

Proof state:
S : Type u_2
inst✝⁷ : CommRing S
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
inst✝ : IsDomain S
hB : IsIntegral R B.gen
x : A
hx : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
⊢ ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ n)) i)

Tactic:
nontriviality A using Subsingleton.elim (x ^ n) 0, isIntegral_zero

Result:
S : Type u_2
inst✝⁷ : CommRing S
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
inst✝ : IsDomain S
hB : IsIntegral R B.gen
x : A
hx : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
a✝ : Nontrivial A
⊢ ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ n)) i)

Proof state:
case refine_1
S : Type u_2
inst✝⁷ : CommRing S
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
inst✝ : IsDomain S
hB : IsIntegral R B.gen
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
a✝ : Nontrivial A
⊢ (fun n =>
      (∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)) →
        ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ n)) i))
    0

Tactic:
intro _ i

Result:
case refine_1
S : Type u_2
inst✝⁷ : CommRing S
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
inst✝ : IsDomain S
hB : IsIntegral R B.gen
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
a✝¹ : Nontrivial A
a✝ : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)
i : Fin B.dim
⊢ IsIntegral R ((B.basis.repr (x ^ 0)) i)

Proof state:
case refine_2
S : Type u_2
inst✝⁷ : CommRing S
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
inst✝ : IsDomain S
hB : IsIntegral R B.gen
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n✝ : ℕ
a✝ : Nontrivial A
n : ℕ
hn :
  ∀ m ≤ n,
    (fun n =>
        (∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)) →
          ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ n)) i))
      m
⊢ (fun n =>
      (∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)) →
        ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ n)) i))
    (n + 1)

Tactic:
intro hx

Result:
case refine_2
S : Type u_2
inst✝⁷ : CommRing S
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
inst✝ : IsDomain S
hB : IsIntegral R B.gen
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n✝ : ℕ
a✝ : Nontrivial A
n : ℕ
hn :
  ∀ m ≤ n,
    (fun n =>
        (∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)) →
          ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ n)) i))
      m
hx : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)
⊢ ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ (n + 1))) i)

Proof state:
case pos
S : Type u_2
inst✝⁷ : CommRing S
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
inst✝ : IsDomain S
hB : IsIntegral R B.gen
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
a✝¹ : Nontrivial A
a✝ : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)
i : Fin B.dim
h✝ : ⟨0, ⋯⟩ = i
⊢ IsIntegral R 1

Tactic:
exact isIntegral_one

Result:
no goals

Proof state:
S : Type u_2
inst✝⁷ : CommRing S
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
inst✝ : IsDomain S
hB : IsIntegral R B.gen
x : A
hx : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
a✝ : Nontrivial A
⊢ ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ n)) i)

Tactic:
revert hx

Result:
S : Type u_2
inst✝⁷ : CommRing S
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
inst✝ : IsDomain S
hB : IsIntegral R B.gen
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
a✝ : Nontrivial A
⊢ (∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)) → ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ n)) i)