-- Mathlib/LinearAlgebra/Matrix/Charpoly/Univ.lean
lemma optionEquivLeft_symm_univ_isHomogeneous :
    ((optionEquivLeft R (n × n)).symm (univ R n)).IsHomogeneous (Fintype.card n)

Proof state:
case h
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i : n, 1
⊢ ∀ i ∈ Finset.univ,
    (↑↑(Equiv.Perm.sign i) *
          ∏ x : n,
            ((Polynomial.aevalTower (rename some) (X none)) (if i x = x then Polynomial.X else 0) -
              X (some (i x, x)))).IsHomogeneous
      (0 + ∑ i : n, 1)

Tactic:
rintro i -

Result:
case h
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i : n, 1
i : Equiv.Perm n
⊢ (↑↑(Equiv.Perm.sign i) *
        ∏ x : n,
          ((Polynomial.aevalTower (rename some) (X none)) (if i x = x then Polynomial.X else 0) -
            X (some (i x, x)))).IsHomogeneous
    (0 + ∑ i : n, 1)

Proof state:
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ ((optionEquivLeft R (n × n)).symm (univ R n)).IsHomogeneous (Fintype.card n)

Tactic:
have aux : Fintype.card n = 0 + ∑ i : n, 1 := by
  simp only [zero_add, Finset.sum_const, smul_eq_mul, mul_one, Fintype.card]

Result:
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i : n, 1
⊢ ((optionEquivLeft R (n × n)).symm (univ R n)).IsHomogeneous (Fintype.card n)

Proof state:
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ Fintype.card n = 0 + ∑ i : n, 1

Tactic:
simp only [zero_add, Finset.sum_const, smul_eq_mul, mul_one, Fintype.card]

Result:
no goals

Proof state:
case pos
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i : n, 1
i : Equiv.Perm n
j : n
h : i j = j
⊢ ((Polynomial.aevalTower (rename some) (X none)) (if i j = j then Polynomial.X else 0) -
        X (some (i j, j))).IsHomogeneous
    1

Tactic:
simp only [h, ↓reduceIte, Polynomial.aevalTower_X, IsHomogeneous.sub, isHomogeneous_X]

Result:
no goals

Proof state:
case h
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i : n, 1
i : Equiv.Perm n
⊢ (↑↑(Equiv.Perm.sign i) *
        ∏ x : n,
          ((Polynomial.aevalTower (rename some) (X none)) (if i x = x then Polynomial.X else 0) -
            X (some (i x, x)))).IsHomogeneous
    (0 + ∑ i : n, 1)

Tactic:
apply IsHomogeneous.mul

Result:
case h.hφ
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i : n, 1
i : Equiv.Perm n
⊢ (↑↑(Equiv.Perm.sign i)).IsHomogeneous 0

case h.hψ
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i : n, 1
i : Equiv.Perm n
⊢ (∏ x : n,
        ((Polynomial.aevalTower (rename some) (X none)) (if i x = x then Polynomial.X else 0) -
          X (some (i x, x)))).IsHomogeneous
    (∑ i : n, 1)

Proof state:
case h.hψ.h
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i : n, 1
i : Equiv.Perm n
⊢ ∀ i_1 ∈ Finset.univ,
    ((Polynomial.aevalTower (rename some) (X none)) (if i i_1 = i_1 then Polynomial.X else 0) -
          X (some (i i_1, i_1))).IsHomogeneous
      1

Tactic:
rintro j -

Result:
case h.hψ.h
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i : n, 1
i : Equiv.Perm n
j : n
⊢ ((Polynomial.aevalTower (rename some) (X none)) (if i j = j then Polynomial.X else 0) -
        X (some (i j, j))).IsHomogeneous
    1

Proof state:
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i : n, 1
⊢ (∑ x : Equiv.Perm n,
        ↑↑(Equiv.Perm.sign x) *
          ∏ x_1 : n,
            ((Polynomial.aevalTower (rename some) (X none)) (if x x_1 = x_1 then Polynomial.X else 0) -
              X (some (x x_1, x_1)))).IsHomogeneous
    (0 + ∑ i : n, 1)

Tactic:
apply IsHomogeneous.sum

Result:
case h
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i : n, 1
⊢ ∀ i ∈ Finset.univ,
    (↑↑(Equiv.Perm.sign i) *
          ∏ x : n,
            ((Polynomial.aevalTower (rename some) (X none)) (if i x = x then Polynomial.X else 0) -
              X (some (i x, x)))).IsHomogeneous
      (0 + ∑ i : n, 1)

Proof state:
case h.hψ.h
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i : n, 1
i : Equiv.Perm n
j : n
⊢ ((Polynomial.aevalTower (rename some) (X none)) (if i j = j then Polynomial.X else 0) -
        X (some (i j, j))).IsHomogeneous
    1

Tactic:
by_cases h : i j = j

Result:
case pos
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i : n, 1
i : Equiv.Perm n
j : n
h : i j = j
⊢ ((Polynomial.aevalTower (rename some) (X none)) (if i j = j then Polynomial.X else 0) -
        X (some (i j, j))).IsHomogeneous
    1

case neg
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i : n, 1
i : Equiv.Perm n
j : n
h : ¬i j = j
⊢ ((Polynomial.aevalTower (rename some) (X none)) (if i j = j then Polynomial.X else 0) -
        X (some (i j, j))).IsHomogeneous
    1

Proof state:
case h.hφ
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i : n, 1
i : Equiv.Perm n
⊢ (↑↑(Equiv.Perm.sign i)).IsHomogeneous 0

Tactic:
apply isHomogeneous_C

Result:
no goals

Proof state:
case neg
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i : n, 1
i : Equiv.Perm n
j : n
h : ¬i j = j
⊢ ((Polynomial.aevalTower (rename some) (X none)) (if i j = j then Polynomial.X else 0) -
        X (some (i j, j))).IsHomogeneous
    1

Tactic:
simp only [h, ↓reduceIte, map_zero, zero_sub, (isHomogeneous_X _ _).neg]

Result:
no goals

Proof state:
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i : n, 1
⊢ ((optionEquivLeft R (n × n)).symm (univ R n)).IsHomogeneous (Fintype.card n)

Tactic:
simp only [aux, univ, charpoly, charmatrix, scalar_apply, RingHom.mapMatrix_apply, det_apply',
  sub_apply, map_apply, of_apply, map_sum, _root_.map_mul, map_intCast, map_prod, map_sub,
  optionEquivLeft_symm_apply, Polynomial.aevalTower_C, rename_X, diagonal, mvPolynomialX]

Result:
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i : n, 1
⊢ (∑ x : Equiv.Perm n,
        ↑↑(Equiv.Perm.sign x) *
          ∏ x_1 : n,
            ((Polynomial.aevalTower (rename some) (X none)) (if x x_1 = x_1 then Polynomial.X else 0) -
              X (some (x x_1, x_1)))).IsHomogeneous
    (0 + ∑ i : n, 1)

Proof state:
case h.hψ
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i : n, 1
i : Equiv.Perm n
⊢ (∏ x : n,
        ((Polynomial.aevalTower (rename some) (X none)) (if i x = x then Polynomial.X else 0) -
          X (some (i x, x)))).IsHomogeneous
    (∑ i : n, 1)

Tactic:
apply IsHomogeneous.prod

Result:
case h.hψ.h
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i : n, 1
i : Equiv.Perm n
⊢ ∀ i_1 ∈ Finset.univ,
    ((Polynomial.aevalTower (rename some) (X none)) (if i i_1 = i_1 then Polynomial.X else 0) -
          X (some (i i_1, i_1))).IsHomogeneous
      1