-- 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:
case neg
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 0

Tactic:
exact isIntegral_zero

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
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)

Tactic:
refine Nat.case_strong_induction_on
  (p := fun n ↦ _ → ∀ (i : Fin B.dim), IsIntegral R (B.basis.repr (x ^ n) i))
  n ?_ fun n hn => ?_

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
⊢ (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

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)

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
a✝ : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)
i : Fin B.dim
⊢ IsIntegral R ((B.basis.repr (x ^ 0)) i)

Tactic:
rw [pow_zero, ← pow_zero B.gen, ← Fin.val_mk B.dim_pos, ← B.basis_eq_pow,
  B.basis.repr_self_apply]

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 (if ⟨0, ⋯⟩ = i then 1 else 0)

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
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)

Tactic:
rw [pow_succ]

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 * x)) 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
a✝ : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)
i : Fin B.dim
⊢ IsIntegral R (if ⟨0, ⋯⟩ = i then 1 else 0)

Tactic:
split_ifs

Result:
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

case neg
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 0

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
hx : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)
⊢ ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ n * x)) i)

Tactic:
exact repr_mul_isIntegral hB (fun _ => hn _ le_rfl (fun _ => hx _) _) hx hmin

Result:
no goals