Theorem: MvPolynomial.homogenization_X_pow_add_C (FltRegular/ReadyForMathlib/Homogenization.lean)

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
⊢ homogenization i (X j ^ n + C r) = X j ^ n + C r * X i ^ n
Tactic:
nontriviality R
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
⊢ homogenization i (X j ^ n + C r) = X j ^ n + C r * X i ^ n

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ homogenization i (X j ^ n + C r) = X j ^ n + C r * X i ^ n
Tactic:
erw [homogenization, Finsupp.mapDomain_add]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ Finsupp.mapDomain (fun j_1 => j_1 + Finsupp.single i ((X j ^ n + C r).totalDegree - j_1.sum fun x m => m)) (X j ^ n) +
      Finsupp.mapDomain (fun j_1 => j_1 + Finsupp.single i ((X j ^ n + C r).totalDegree - j_1.sum fun x m => m)) (C r) =
    X j ^ n + C r * X i ^ n

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ Finsupp.mapDomain (fun j_1 => j_1 + Finsupp.single i ((X j ^ n + C r).totalDegree - j_1.sum fun x m => m)) (X j ^ n) +
      Finsupp.mapDomain (fun j_1 => j_1 + Finsupp.single i ((X j ^ n + C r).totalDegree - j_1.sum fun x m => m)) (C r) =
    X j ^ n + C r * X i ^ n
Tactic:
erw [AddMonoidAlgebra.single_pow]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ Finsupp.mapDomain
        (fun j_1 =>
          j_1 +
            Finsupp.single i
              ((AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r).totalDegree - j_1.sum fun x m => m))
        (AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n)) +
      Finsupp.mapDomain
        (fun j_1 =>
          j_1 +
            Finsupp.single i
              ((AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r).totalDegree - j_1.sum fun x m => m))
        (C r) =
    AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r * X i ^ n

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ Finsupp.mapDomain
        (fun j_1 =>
          j_1 +
            Finsupp.single i
              ((AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r).totalDegree - j_1.sum fun x m => m))
        (AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n)) +
      Finsupp.mapDomain
        (fun j_1 =>
          j_1 +
            Finsupp.single i
              ((AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r).totalDegree - j_1.sum fun x m => m))
        (C r) =
    AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r * X i ^ n
Tactic:
erw [Finsupp.mapDomain_single, Finsupp.mapDomain_single]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ Finsupp.single
        (n • Finsupp.single j 1 +
          Finsupp.single i
            ((AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r).totalDegree -
              (n • Finsupp.single j 1).sum fun x m => m))
        (1 ^ n) +
      Finsupp.single
        (0 +
          Finsupp.single i
            ((AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r).totalDegree - Finsupp.sum 0 fun x m => m))
        r =
    AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r * X i ^ n

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ Finsupp.single
        (n • Finsupp.single j 1 +
          Finsupp.single i
            ((AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r).totalDegree -
              (n • Finsupp.single j 1).sum fun x m => m))
        (1 ^ n) +
      Finsupp.single
        (0 +
          Finsupp.single i
            ((AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r).totalDegree - Finsupp.sum 0 fun x m => m))
        r =
    AddMonoidAlgebra.single (n • Finsupp.single j 1) (1 ^ n) + C r * X i ^ n
Tactic:
simp only [tsub_zero, Finsupp.sum_zero_index, Finsupp.sum_single_index, zero_add,
  single_eq_monomial, one_pow, mul_one, Finsupp.smul_single', Finsupp.single_tsub]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ (monomial
          (Finsupp.single j n +
            (Finsupp.single i ((monomial (Finsupp.single j n)) 1 + C r).totalDegree - Finsupp.single i n)))
        1 +
      (monomial (Finsupp.single i ((monomial (Finsupp.single j n)) 1 + C r).totalDegree)) r =
    (monomial (Finsupp.single j n)) 1 + C r * X i ^ n

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ (monomial
          (Finsupp.single j n +
            (Finsupp.single i ((monomial (Finsupp.single j n)) 1 + C r).totalDegree - Finsupp.single i n)))
        1 +
      (monomial (Finsupp.single i ((monomial (Finsupp.single j n)) 1 + C r).totalDegree)) r =
    (monomial (Finsupp.single j n)) 1 + C r * X i ^ n
Tactic:
congr
State after:
case e_a.e_a.e_s
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ Finsupp.single j n + (Finsupp.single i ((monomial (Finsupp.single j n)) 1 + C r).totalDegree - Finsupp.single i n) =
    Finsupp.single j n

case e_a
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ (monomial (Finsupp.single i ((monomial (Finsupp.single j n)) 1 + C r).totalDegree)) r = C r * X i ^ n

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
⊢ (X j ^ n + C r).totalDegree = n
Tactic:
rw [totalDegree_add_eq_left_of_totalDegree_lt]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
⊢ (X j ^ n).totalDegree = n

R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
⊢ (C r).totalDegree < (X j ^ n).totalDegree

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
⊢ (X j ^ n).totalDegree = n
Tactic:
exact totalDegree_X_pow _ _
State after:
no goals

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
⊢ (C r).totalDegree < (X j ^ n).totalDegree
Tactic:
simp only [totalDegree_C, totalDegree_X_pow, hn]
State after:
no goals

State before:
case e_a.e_a.e_s
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ Finsupp.single j n + (Finsupp.single i ((monomial (Finsupp.single j n)) 1 + C r).totalDegree - Finsupp.single i n) =
    Finsupp.single j n
Tactic:
rw [totalDegree_add_eq_left_of_totalDegree_lt]
State after:
case e_a.e_a.e_s
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ Finsupp.single j n + (Finsupp.single i ((monomial (Finsupp.single j n)) 1).totalDegree - Finsupp.single i n) =
    Finsupp.single j n

case e_a.e_a.e_s
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ (C r).totalDegree < ((monomial (Finsupp.single j n)) 1).totalDegree

State before:
case e_a.e_a.e_s
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ Finsupp.single j n + (Finsupp.single i ((monomial (Finsupp.single j n)) 1).totalDegree - Finsupp.single i n) =
    Finsupp.single j n

case e_a.e_a.e_s
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ (C r).totalDegree < ((monomial (Finsupp.single j n)) 1).totalDegree
Tactic:
simp [one_ne_zero]
State after:
case e_a.e_a.e_s
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ (C r).totalDegree < ((monomial (Finsupp.single j n)) 1).totalDegree

State before:
case e_a.e_a.e_s
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ (C r).totalDegree < ((monomial (Finsupp.single j n)) 1).totalDegree
Tactic:
simp [one_ne_zero, hn]
State after:
no goals

State before:
case e_a
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ (monomial (Finsupp.single i ((monomial (Finsupp.single j n)) 1 + C r).totalDegree)) r = C r * X i ^ n
Tactic:
convert (C_mul_X_pow_eq_monomial (R := R)).symm
State after:
case h.e'_3.h.e'_6.h.e'_6
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ n = ((monomial (Finsupp.single j n)) 1 + C r).totalDegree

State before:
case h.e'_3.h.e'_6.h.e'_6
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ n = ((monomial (Finsupp.single j n)) 1 + C r).totalDegree
Tactic:
rw [← C_mul_X_pow_eq_monomial]
State after:
case h.e'_3.h.e'_6.h.e'_6
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ n = (C 1 * X j ^ n + C r).totalDegree

State before:
case h.e'_3.h.e'_6.h.e'_6
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
this : (X j ^ n + C r).totalDegree = n
⊢ n = (C 1 * X j ^ n + C r).totalDegree
Tactic:
simp [this]
State after:
no goals