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

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial ι R
hp : p ≠ 0
h : Disjoint p.support q.support
⊢ p + q ≠ 0
Tactic:
classical
contrapose! hp
have := congr_arg support hp
rw [support_zero, support_add_eq h,
  Finset.union_eq_empty,MvPolynomial.support_eq_empty] at this
exact this.left
State after:
no goals

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial ι R
hp : p ≠ 0
h : Disjoint p.support q.support
⊢ p + q ≠ 0
Tactic:
contrapose! hp
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial ι R
h : Disjoint p.support q.support
hp : p + q = 0
⊢ p = 0

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial ι R
h : Disjoint p.support q.support
hp : p + q = 0
⊢ p = 0
Tactic:
have := congr_arg support hp
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial ι R
h : Disjoint p.support q.support
hp : p + q = 0
this : (p + q).support = support 0
⊢ p = 0

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial ι R
h : Disjoint p.support q.support
hp : p + q = 0
this : (p + q).support = support 0
⊢ p = 0
Tactic:
rw [support_zero, support_add_eq h,
  Finset.union_eq_empty,MvPolynomial.support_eq_empty] at this
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial ι R
h : Disjoint p.support q.support
hp : p + q = 0
this : p = 0 ∧ q.support = ∅
⊢ p = 0

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial ι R
h : Disjoint p.support q.support
hp : p + q = 0
this : p = 0 ∧ q.support = ∅
⊢ p = 0
Tactic:
exact this.left
State after:
no goals