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

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

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

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
this : (X j + C r).totalDegree = 1
⊢ Finsupp.single
        (Finsupp.single j 1 + Finsupp.single i ((X j + C r).totalDegree - (Finsupp.single j 1).sum fun x m => m)) 1 +
      Finsupp.single (0 + Finsupp.single i ((X j + C r).totalDegree - Finsupp.sum 0 fun x m => m)) r =
    X j + C r * X i
Tactic:
simp only [tsub_zero, Finsupp.sum_zero_index, Finsupp.sum_single_index, this, add_zero,
  Finsupp.single_zero, zero_add, single_eq_monomial]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
this : (X j + C r).totalDegree = 1
⊢ (monomial (Finsupp.single j 1 + Finsupp.single i (1 - 1))) 1 + (monomial (Finsupp.single i 1)) r = X j + C r * X i

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
this : (X j + C r).totalDegree = 1
⊢ (monomial (Finsupp.single j 1 + Finsupp.single i (1 - 1))) 1 + (monomial (Finsupp.single i 1)) r = X j + C r * X i
Tactic:
rw [X, X, ← C_mul_X_pow_eq_monomial, pow_one]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
this : (X j + C r).totalDegree = 1
⊢ (monomial (Finsupp.single j 1 + Finsupp.single i (1 - 1))) 1 + C r * X i =
    (monomial (Finsupp.single j 1)) 1 + C r * (monomial (Finsupp.single i 1)) 1

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

State before:
case e_a.e_a.e_s
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
this : (X j + C r).totalDegree = 1
⊢ Finsupp.single j 1 + Finsupp.single i (1 - 1) = Finsupp.single j 1
Tactic:
simp
State after:
no goals

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

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

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
⊢ (X j).totalDegree = 1
Tactic:
exact totalDegree_X _
State after:
no goals

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
⊢ (C r).totalDegree < (X j).totalDegree
Tactic:
simp only [totalDegree_C, totalDegree_X, Nat.lt_one_iff]
State after:
no goals